<commit_before>\section{Language}


\newcommand{\SC}{\textsc}
\newcommand{\lgb}{\langle}
\newcommand{\rgb}{\rangle}
\newcommand{\gb}[1]{\left<{#1}\right>}
\[
\begin{array}{rll}
\SC{InTm} ::= & \verb!*! & \mbox{Set} \\
            | & \lgb\verb!(!\SC{Nom}\verb! : !\SC{InTm} \verb!)!\rgb^+\verb! -> ! \SC{InTm} 
                & \mbox{\(\Pi\)-type}\\
            | & \SC{InTm} \verb! -> ! \SC{InTm}  & \mbox{nondependent function type}\\
            | & \verb!\! \SC{Nom}^* \verb! -> ! \SC{InTm} & \mbox{\(\lambda\)-abstraction}\\
            | & \verb!#! & \mbox{Prop} \\
            | & \verb!:- ! \SC{InTm} & \mbox{set of proofs} \\
            | & \verb!(!\SC{Sig}\verb!)! & \mbox{`record' signature} \\
            | & \verb![]! & \mbox{void}\\
            | & \verb![!\SC{InTm}^+\:\lgb\verb!/ !\SC{InTm}\rgb^?\verb!]! & \mbox{tuple}\\
            | & \verb!{!\SC{Nom}^*\:\lgb\verb!/ !\SC{InTm}\rgb^?\verb!}! &
 \mbox{enumeration}\\
            | & \verb!(!\SC{InTm}\verb!)! & \mbox{grouping} \\
            | & \SC{ExTm} & \mbox{term with synthesizable type} \medskip \\
\SC{Sig} ::= & \varepsilon & \mbox{unit signature} \\
           | & \lgb\SC{Nom}\verb! : !\rgb^? \SC{InTm}\:
               \lgb\verb!; !|\verb!:- !\rgb \lgb\SC{InTm}|\SC{Sig}\rgb
                  & \mbox{\(\Sigma\)-type} \medskip \\
\SC{ExTm} ::= & \SC{InTm}\verb! : !\SC{InTm} \\
            | & \SC{Nom}\lgb\verb!^!\SC{Nat}\rgb \\
            | & \SC{ExTm}\:\SC{InTm} \\
            | & \SC{ExTm}\:\verb|!| & \mbox{car} \\
            | & \SC{ExTm}\:\verb!-! & \mbox{cdr} \\
\end{array}
\]

and more to come.


<commit_msg>Extend language definition with Prop subset, operator, nat, and Con.<commit_after>\section{Language}


\newcommand{\SC}{\textsc}
\newcommand{\lgb}{\langle}
\newcommand{\rgb}{\rangle}
\newcommand{\gb}[1]{\left<{#1}\right>}
\[
\begin{array}{rll}
\SC{InTm} ::= & \verb!*! 
                & \mbox{Set} \\
            | & \lgb\verb!(!\SC{Nom}\verb! : !\SC{InTm} \verb!)!\rgb^+\verb! -> ! \SC{InTm} 
                & \mbox{\(\Pi\)-type} \\
            | & \SC{InTm} \verb! -> ! \SC{InTm}  
                & \mbox{nondependent function type} \\
            | & \verb!\! \SC{Nom}^* \verb! -> ! \SC{InTm} 
                & \mbox{\(\lambda\)-abstraction} \\
            | & \verb!#! 
                & \mbox{Prop} \\
            | & \verb!:- ! \SC{InTm} 
                & \mbox{set of proofs} \\
            | & \SC{NAT} \lgb\verb!+ ! \SC{InTm}\rgb^? 
                & \mbox{Integers} \\
            | & \verb!@! \SC{InTm} 
                & \mbox{Con for inductive definitions} \\
            | & \verb!(!\SC{Sig}\verb!)! 
                & \mbox{`record' signature} \\
            | & \verb![]! 
                & \mbox{void} \\
            | & \verb![!\SC{InTm}^+\:\lgb\verb!/ !\SC{InTm}\rgb^?\verb!]! 
                & \mbox{tuple} \\
            | & \verb!{!\SC{Nom}^{\verb!,!*}\:\lgb\verb!/ !\SC{InTm}\rgb^?\verb!}! 
                & \mbox{enumeration} \\
            | & \lgb\verb!(!\SC{Nom}\verb! : !\SC{InTm} \verb!)!\rgb^+\verb! => ! \SC{InTm} 
                & \mbox{propositional \(\forall\)} \\
            | & \SC{InTm} \verb! && ! \SC{InTm} 
                & \mbox{propositional And} \\
            | & \verb!TT ! | \verb| FF|
                & \mbox{propositional Trivial and Absurd} \\
            | & \verb!(!\SC{InTm}\verb! : !\SC{InTm}\verb!)! \verb! == ! \verb!(!\SC{InTm}\verb! : !\SC{InTm}\verb!)! 
                & \mbox{blue equality} \\
            | & \verb!(!\SC{InTm}\verb!)! 
                & \mbox{grouping} \\
            | & \SC{ExTm} 
                & \mbox{term with synthesizable type} \medskip \\
\SC{Sig} ::= & \varepsilon & \mbox{unit signature} \\
           | & \lgb\SC{Nom}\verb! : !\rgb^? \SC{InTm}\:
               \lgb\verb!; !|\verb! :- !\rgb \lgb\SC{InTm}|\SC{Sig}\rgb
                  & \mbox{\(\Sigma\)-type} \medskip \\
\SC{ExTm} ::= & \SC{InTm}\verb! : !\SC{InTm} 
                & \\
            | & \SC{Nom}\lgb\verb!^!\SC{Nat}\rgb 
                & \\
            | & \SC{ExTm}\:\SC{InTm} 
                & \\
            | & \SC{ExTm}\:\verb|!| 
                & \mbox{car} \\
            | & \SC{ExTm}\:\verb!-! 
                & \mbox{cdr} \\
            | & \SC{Op}\verb!(!\SC{InTm}^{\verb!,!*}\verb!)! 
                & \mbox{operator} \\
            | & \verb!(!\SC{InTm}\verb! : !\SC{InTm}\verb!)!  \verb! <-> ! \verb!(!\SC{InTm}\verb! : !\SC{InTm}\verb!)! 
                & \mbox{green equality} \\
            
\end{array}
\]

and more to come.



{'fraction_non_alphanumeric': 0.26601855943437913, 'fraction_numerical': 0.0008837825894829872, 'mean_word_length': 1.4260450160771705, 'pattern_counts': {'":': 0, '<': 6, '<?xml version=': 0, '>': 13, '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': '4899132', 'n_tokens_mistral': 1846, 'n_tokens_neox': 1742, 'n_words': 209}