Przemebra/praca-magisterska/agda-tex/IdTex.tex

\begin{code}%
%% \>[0]\AgdaSymbol{\{{-}\#}\AgdaSpace{}%
%% \AgdaKeyword{OPTIONS}\AgdaSpace{}%
%% \AgdaOption{{-}{-}allow{-}unsolved{-}metas}\AgdaSpace{}%
%% \AgdaSymbol{\#{-}\}}\<%
%% \\
%% %
%% \\[\AgdaEmptyExtraSkip]%
%% \>[0]\AgdaKeyword{module}\AgdaSpace{}%
%% \AgdaModule{IdTex}\AgdaSpace{}%
%% \AgdaKeyword{where}\<%
%% \\
%% \>[0]\AgdaKeyword{open}\AgdaSpace{}%
%% \AgdaKeyword{import}\AgdaSpace{}%
%% \AgdaModule{Level}\AgdaSpace{}%
%% \AgdaKeyword{using}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaPostulate{Level}\AgdaSymbol{)}\<%
%% \\
%% \>[0]\AgdaKeyword{open}\AgdaSpace{}%
%% \AgdaKeyword{import}\AgdaSpace{}%
%% \AgdaModule{latex.Nat}\<%
%% \\
%% %
%% \\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaKeyword{data}\AgdaSpace{}%
\AgdaDatatype{Id}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{a}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPostulate{Level}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSpace{}%
\AgdaBound{a}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSpace{}%
\AgdaBound{a}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[2]\AgdaKeyword{instance}\AgdaSpace{}%
\AgdaInductiveConstructor{refl}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{x}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaBound{A}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{Id}\AgdaSpace{}%
\AgdaBound{x}\AgdaSpace{}%
\AgdaBound{x}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaFunction{0{-}eq{-}0}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{Id}\AgdaSpace{}%
\AgdaInductiveConstructor{0\#}\AgdaSpace{}%
\AgdaInductiveConstructor{0\#}\<%
\\
\>[0]\AgdaFunction{0{-}eq{-}0}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{refl}\AgdaSpace{}%
\AgdaInductiveConstructor{0\#}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaFunction{1{-}eq{-}0}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{Id}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaInductiveConstructor{suc}\AgdaSpace{}%
\AgdaInductiveConstructor{0\#}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaInductiveConstructor{0\#}\<%
\\
\>[0]\AgdaFunction{1{-}eq{-}0}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaSymbol{\{!!\}}\<%
\\
\>[0]\<%
\end{code}