<commit_before>\section{Skeleton feature}

%if False

> {-# OPTIONS_GHC -F -pgmF she #-}

> module Features.Skeleton where

%endif


> import -> CanConstructors where

> import -> TraverseCan where

> import -> HalfZipCan where

> import -> Primitives where

> import -> CanPats where

> import -> DisplayCanPats where

> import -> SugarTactics where

> import -> CanPretty where

> import -> CanTyRules where

> import -> ElimTyRules where

> import -> Operators where

> import -> OpCompile where

> import -> OpCode where

> import -> ElaborateRules where
 
> import -> DistillRules where<commit_msg>Features/Skeleton: an hopefully complete Feature skeleton<commit_after>\section{Skeleton feature}

%if False

> {-# OPTIONS_GHC -F -pgmF she #-}

> module Features.Skeleton where

%endif


\subsection{Plugging Canonical terms in}

> import -> CanConstructors where

> import -> CanPretty where

> import -> CanTyRules where

> import -> CanCompile where

> import -> EtaExpand where

> import -> CanPats where

> import -> DisplayCanPats where

> import -> TraverseCan where

> import -> HalfZipCan where

\subsection{Plugging Eliminators in}

> import -> ElimTyRules where

> import -> ElimComputation where

> import -> ElimCompile where

> import -> TraverseElim where

> import -> ElimPretty where

\subsection{Plugging Operators in}

> import -> Operators where

> import -> OpCompile where

> import -> OpCode where

\subsection{Plugging Axioms in}

> import -> Axioms where

> import -> AxCode where

\subsection{Extending the type-checker}

> import -> Check where

\subsection{Extending the equality}

> import -> OpRunEqGreen where

> import -> Coerce where

\subsection{Extending the quotient}

> import -> QuotientDefinitions where

\subsection{Extending the Display Language}

> import -> ElaborateRules where
 
> import -> DistillRules where

> import -> InDTmConstructors where

> import -> InDTmPretty where

> import -> Pretty where

\subsection{Adding Primitive references in Cochon}

> import -> Primitives where

\subsection{Extending the Mangler}

> import -> DMangleRules where

\subsection{Extending the Term Builder}

> import -> SugarTactics where
{'fraction_non_alphanumeric': 0.09747126436781609, 'fraction_numerical': 0.0, 'mean_word_length': 3.900900900900901, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 99, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7525807', 'n_tokens_mistral': 690, 'n_tokens_neox': 664, 'n_words': 204}