% \iffalse
%<*driver>
\def\stexdocpath{../../doc}
\input{\stexdocpath/stex-docheader}
\stextoptitle{The \sTeX Package}{stex}
\docmodule
%</driver>
%<*package>
% \fi
%
% \begin{sfragment}{Metatheory}
%
% \begin{implementation}
%    \begin{macrocode}
%<@@=stex_meta>
%    \end{macrocode}
%
% Setup:
%    \begin{macrocode}
\group_begin:
\cs_set:Npn \__stex_modules_persist_module: {}
\cs_set:Npn \stex_check_term:nn #1 #2 {}
\cs_set:Npn \_stex_sref_do_aux:n #1 { #1 }
\bool_set_false:N \c_stex_check_terms_bool
\bool_set_false:N \l__stex_annotate_do_output_bool
\tl_if_exist:cF {c_stex_mathhub_FTML/meta_archive}{
  \tl_gset:ce {c_stex_mathhub_FTML/meta_archive}{
    {\tl_to_str:n{FTML/meta}}
    {\tl_to_str:n{http://mathhub.info}}
    {}
  }
}
\tl_set:Ne \l_stex_current_document_uri {
  {\tl_to_str:n{FTML/meta}}{}
  {\tl_to_str:n{Metatheory}}{\tl_to_str:n{en}}{}
}
\_stex_module_setup_top_nosig:n{Metatheory}
\g_stex_every_module_tl
%    \end{macrocode}
% \end{implementation}
%
% \begin{documentation} TODO \end{documentation}
%
% \begin{implementation}
%    \begin{macrocode}
\symdef{of~type}[args=ii,invisible]{#1}
\notation{of~type}[colon]{#1 \mathbin{\comp{:}} #2}

\symdef{apply}[args=ia,prec=0;\infprec x\infprec]{#1\mathopen{\comp(} #2 \mathclose{\comp)}}
\notation{apply}[lambda]{#1\; \argsep{#2}{\;}}
\notation{apply}[infixop]{\argsep{#2}{\mathbin{#1}}\STEXinvisible{#1}}
\notation{apply}[infixrel]{\argsep{#2}{\mathrel{#1}}\STEXinvisible{#1}}

% structures
\symdef{module~type}[args=i,op=\mathtt{MOD}]
  {\mathopen{\comp{\mathtt{MOD}(}}#1\mathclose{\comp{)}}}
\symdef{module~type~merge}[args=a,op=\oplus]
  {\argsep{#1}{\mathbin{\comp{\oplus}}}}
\symdef{anonymous~record}[args=a]
  {\mathopen{\comp{[[}}#1\mathclose{\comp{]]}}}
\symdef{record~field}[args=2]{#1\comp{.}#2}
\symdecl*{record~type}

\symdecl{mathstruct}[name=mathematical~structure,args=a] % TODO
\notation{mathstruct}[angle,prec=nobrackets]
  {\mathopen{\comp\langle} #1 \mathclose{\comp\rangle}}
\notation{mathstruct}[parens,prec=nobrackets]
  {\mathopen{\comp(} #1 \mathclose{\comp)}}

% sequences
\symdef{ellipses}[ldots]{\ldots}
\symdef{sequence~expression}[comma,args=a]{#1}
\symdef{sequence~type}[args=1]{#1^{\comp\ast}}
\symdef{sequence~map}[args=ia]{
  \comp{\mathrm{map}}\mathopen{\comp{(}}#1\mathpunct{\comp{,}}
  #2\mathclose{\comp{)}}
}

\symdecl{bind}[args=Bi,assoc=pre]
\notation{bind}[depfun,prec=nobrackets,op=(\cdot)\;\to\;\cdot]
  {\mathopen{\comp(} #1 \mathclose{\comp{)}\mathbin{\comp{\to}}} #2}
\notation{bind}[forall]{\comp\forall #1.\;#2}
\notation{bind}[Pi]{\mathop{\comp\prod}\c_math_subscript_token{#1}#2}

\symdef{implicit~bind}[args=Bi,assoc=pre]{\mathopen{\comp\{} #1 \mathclose{\comp{\}\c_math_subscript_token I}} #2}

\symdecl*{integer~literal}
\notation{integer~literal}{\mathbb Z}

\symdecl*{ordinal}
\notation{ordinal}{\mathtt{Ord}}

% propositions
\symdef{prop}[name=proposition]{\mathtt{Prop}}
\symdef{judgment~holds}[args=i,role=judgment]{\comp\vdash\;#1}

% any object
\symdef{object}{\mathtt{Obj}}

% TODO DELETE
\symdef{aseqdots}[args=a,prec=nobrackets]
  {#1\comp{,\ldots}}%{##1\comp,##2}
\symdef{aseqfromto}[args=ai,prec=nobrackets]
  {#1\comp{,\ldots,}#2}%{##1\comp,##2}
\symdef{aseqfromtovia}[args=aii,prec=nobrackets]
  {#1\comp{,\ldots,}#2\comp{,\ldots,}#3}%{##1\comp,##2}
%    \end{macrocode}
% \end{implementation}
% 
%
%
% \begin{implementation}
% Closing:
%    \begin{macrocode}
\global \let \l_stex_metatheory_uri \l_stex_current_module_uri
\global \let \c_stex_default_metatheory \l_stex_metatheory_uri
\stex_close_module:
\group_end:
%    \end{macrocode}
% \end{implementation}
%
% \end{sfragment}