<commit_before>\section{UId}

%if False

> {-# OPTIONS_GHC -F -pgmF she #-}
> {-# LANGUAGE TypeOperators, GADTs, KindSignatures,
>     TypeSynonymInstances, FlexibleInstances, ScopedTypeVariables #-}

> module UId where

%endif

> import -> CanConstructors where
>   UId    :: Can t
>   Tag    :: String -> Can t

> import -> CanPats where
>   pattern UID = C UId
>   pattern TAG s = C (Tag s)

> import -> TraverseCan where
>   traverse f UId          = (|EnumU|)
>   traverse f (Tag s)      = (|(Tag s)|)

> import -> CanTyRules where
>   canTy _  (Set :>: UId)    = return UId
>   canTy _  (UId :>: Tag s)  = return (Tag s)

> import -> OpRunEqGreen where
>   opRunEqGreen [UID,TAG s1,UID,TAG s2] | s1 == s2 = Right $ TRIVIAL
>   opRunEqGreen [UID,TAG _,UID,TAG _] = Right $ ABSURD
<commit_msg>UId: documentation<commit_after>\section{UId}

%if False

> {-# OPTIONS_GHC -F -pgmF she #-}
> {-# LANGUAGE TypeOperators, GADTs, KindSignatures,
>     TypeSynonymInstances, FlexibleInstances, ScopedTypeVariables #-}

> module UId where

%endif

Formation rule:

\begin{prooftree}
\AxiomC{}
\RightLabel{UId-formation}
\UnaryInfC{|Set :>: UId|}
\end{prooftree}

Introduction rules:

\begin{prooftree}
\AxiomC{}
\RightLabel{UId-intro-1}
\UnaryInfC{|UId :>: Tag s|}
\end{prooftree}

\begin{prooftree}
\AxiomC{|s1 == s2|}
\RightLabel{UId-intro-2}
\UnaryInfC{|UId :>: (Tag s1 == Tag s2)|}
\end{prooftree}

> import -> CanConstructors where
>   UId    :: Can t
>   Tag    :: String -> Can t

> import -> CanPats where
>   pattern UID = C UId
>   pattern TAG s = C (Tag s)

> import -> TraverseCan where
>   traverse f UId          = (|EnumU|)
>   traverse f (Tag s)      = (|(Tag s)|)

> import -> CanTyRules where
>   canTy _  (Set :>: UId)    = return UId
>   canTy _  (UId :>: Tag s)  = return (Tag s)

> import -> OpRunEqGreen where
>   opRunEqGreen [UID,TAG s1,UID,TAG s2] | s1 == s2 = Right $ TRIVIAL
>   opRunEqGreen [UID,TAG _,UID,TAG _] = Right $ ABSURD

{'fraction_non_alphanumeric': 0.15250767656090072, 'fraction_numerical': 0.007164790174002047, 'mean_word_length': 3.168443496801706, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 60, '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': '5232006', 'n_tokens_mistral': 818, 'n_tokens_neox': 792, 'n_words': 198}