% \iffalse meta-comment % An Infrastructure for Semantic Macros and Module Scoping % Copyright (c) 2019 Michael Kohlhase, all rights reserved % this file is released under the % LaTeX Project Public License (LPPL) % % The original of this file is in the public repository at % http://github.com/sLaTeX/sTeX/ % % TODO update copyright % %<*driver> \def\libfolder#1{../../lib/#1} \input{../../doc/stex-docheader} \begin{document} \DocInput{\jobname.dtx} \end{document} % % \fi % % \title{ \sTeX-Metatheory % \thanks{Version {\fileversion} (last revised {\filedate})} % } % % \author{Michael Kohlhase, Dennis Müller\\ % FAU Erlangen-Nürnberg\\ % \url{http://kwarc.info/} % } % % \maketitle % %\ifinfulldoc\else % This is the documentation for the \pkg{stex-metatheory} package. % For a more high-level introduction, % see \href{\basedocurl/manual.pdf}{the \sTeX Manual} or the % \href{\basedocurl/stex.pdf}{full \sTeX documentation}. % % \input{../../doc/packages/stex-metatheory} % \fi % % \begin{documentation}\label{pkg:metatheory:doc} % % \section{Symbols}\label{pkg:metatheory:symbols} % % \end{documentation} % % \begin{implementation}\label{pkg:metatheory:impl} % % \section{\sTeX-Metatheory Implementation} % % \begin{macrocode} %<*package> %<@@=stex_modules> %%%%%%%%%%%%% metatheory.dtx %%%%%%%%%%%%% \str_const:Nn \c_stex_metatheory_ns_str {http://mathhub.info/sTeX/meta} \begingroup \stex_module_setup:nn{ ns=\c_stex_metatheory_ns_str, meta=NONE }{Metatheory} \stex_reactivate_macro:N \symdecl \stex_reactivate_macro:N \notation \stex_reactivate_macro:N \symdef \ExplSyntaxOff \csname stex_suppress_html:n\endcsname{ % is-a (a:A, a \in A, a is an A, etc.) \symdecl{isa}[args=ai] \notation{isa}[typed,op=:]{#1 \comp{:} #2}{##1 \comp, ##2} \notation{isa}[in]{#1 \comp\in #2}{##1 \comp, ##2} \notation{isa}[pred]{#2\comp(#1 \comp)}{##1 \comp, ##2} % bind (\forall, \Pi, \lambda etc.) \symdecl{bind}[args=Bi,assoc=pre] \notation{bind}[depfun,prec=nobrackets,op={(\cdot)\;\to\;\cdot}]{\comp( #1 \comp{)\;\to\;} #2}{##1 \comp, ##2} \notation{bind}[forall]{\comp\forall #1.\;#2}{##1 \comp, ##2} \notation{bind}[Pi]{\comp\prod_{#1}#2}{##1 \comp, ##2} % implicit bind \symdecl{implicitbind}[args=Bi,assoc=pre] \notation{implicitbind}[braces,prec=nobrackets,op={\{\cdot\}_I\;\cdot}]{\comp\{ #1 \comp{\}_I\;} #2}{##1 \comp, ##2} \notation{implicitbind}[depfun,prec=nobrackets]{\comp( #1 \comp{)\;\to_I\;} #2}{##1 \comp, ##2} \notation{implicitbind}[Pi]{\comp\prod^I_{#1}#2}{##1\comp,##2} % dummy variable \symdecl{dummyvar} \notation{dummyvar}[underscore]{\comp\_} \notation{dummyvar}[dot]{\comp\cdot} \notation{dummyvar}[dash]{\comp{{\rm --}}} %fromto (function space, Hom-set, implication etc.) \symdecl{fromto}[args=ai] \notation{fromto}[xarrow]{#1 \comp\to #2}{##1 \comp\times ##2} \notation{fromto}[arrow]{#1 \comp\to #2}{##1 \comp\to ##2} % mapto (lambda etc.) %\symdecl{mapto}[args=Bi] %\notation{mapto}[mapsto]{#1 \comp\mapsto #2}{#1 \comp, #2} %\notation{mapto}[lambda]{\comp\lambda #1 \comp.\; #2}{#1 \comp, #2} %\notation{mapto}[lambdau]{\comp\lambda_{#1} \comp.\; #2}{#1 \comp, #2} % function/operator application \symdecl{apply}[args=ia] \notation{apply}[prec=0;0x\infprec,parens,op=\cdot(\cdot)]{#1 \comp( #2 \comp)}{##1 \comp, ##2} \notation{apply}[prec=0;0x\infprec,lambda]{#1 \; #2 }{##1 \; ##2} % collection of propositions/booleans/truth values \symdecl{prop}[name=proposition] \notation{prop}[prop]{\comp{{\rm prop}}} \notation{prop}[BOOL]{\comp{{\rm BOOL}}} \symdecl{judgmentholds}[args=1] \notation{judgmentholds}[vdash,op=\vdash]{\comp\vdash\; #1} % sequences \symdecl{seqtype}[args=1] \notation{seqtype}[kleene]{#1^{\comp\ast}} \symdecl{seqexpr}[args=a] \notation{seqexpr}[angle,prec=nobrackets]{\comp\langle #1\comp\rangle}{##1\comp,##2} \symdef{seqmap}[args=abi,setlike]{\comp\{#3 \comp| #2\comp\in \dobrackets{#1} \comp\}}{##1 \comp, ##2} \symdef{seqprepend}[args=ia]{#1 \comp{::} #2}{##1 \comp, ##2} \symdef{seqappend}[args=ai]{#1 \comp{::} #2}{##1 \comp, ##2} \symdef{seqfoldleft}[args=iabbi]{ \comp{foldl}\dobrackets{#1,#2}\dobrackets{#3\comp,#4\comp\mapsto#5}}{##1 \comp, ##2} \symdef{seqfoldright}[args=iabbi,op=foldr]{ \comp{foldr}\dobrackets{#1,#2}\dobrackets{#3\comp,#4\comp\mapsto#5}}{##1 \comp, ##2} \symdef{seqhead}[args=a]{\comp{head}\dobrackets{#1}}{##1 \comp, ##2} \symdef{seqtail}[args=a]{\comp{tail}\dobrackets{#1}}{##1 \comp, ##2} \symdef{seqlast}[args=a]{\comp{last}\dobrackets{#1}}{##1 \comp, ##2} \symdef{seqinit}[args=a]{\comp{tail}\dobrackets{#1}}{##1 \comp, ##2} \symdef{sequence-index}[args=2,li,prec=nobrackets]{{#1}_{#2}} \notation{sequence-index}[ui,prec=nobrackets]{{#1}^{#2}} \symdef{aseqdots}[args=a,prec=nobrackets]{#1\comp{,\ellipses}}{##1\comp,##2} \symdef{aseqfromto}[args=ai,prec=nobrackets]{#1\comp{,\ellipses,}#2}{##1\comp,##2} \symdef{aseqfromtovia}[args=aii,prec=nobrackets]{#1\comp{,\ellipses,}#2\comp{,\ellipses,}#3}{##1\comp,##2} % nat literals \symdef{natliteral}{\comp{\mathtt{Ord}}} % letin (``let'', local definitions, variable substitution) \symdecl{letin}[args=bii] \notation{letin}[let]{\comp{{\rm let}}\;#1\comp{=}#2\;\comp{{\rm in}}\;#3} \notation{letin}[subst]{#3 \comp[ #1 \comp/ #2 \comp]} \notation{letin}[frac]{#3 \comp[ \frac{#2}{#1} \comp]} % structures \symdecl*{module-type}[args=1] \notation{module-type}{\comp{\mathtt{MOD}} #1} \symdecl{mathstruct}[name=mathematical-structure,args=a] % TODO \notation{mathstruct}[angle,prec=nobrackets]{\comp\langle #1 \comp\rangle}{##1 \comp, ##2} % objects \symdecl{object} \notation{object}{\comp{\mathtt{OBJECT}}} } % The following are abbreviations in the sTeX corpus that are left over from earlier % developments. They will eventually be phased out. \ExplSyntaxOn \stex_add_to_current_module:n{ \def\nappli#1#2#3#4{\apply{#1}{\naseqli{#2}{#3}{#4}}} \def\nappui#1#2#3#4{\apply{#1}{\nasequi{#2}{#3}{#4}}} \def\livar{\csname sequence-index\endcsname[li]} \def\uivar{\csname sequence-index\endcsname[ui]} \def\naseqli#1#2#3{\aseqfromto{\livar{#1}{#2}}{\livar{#1}{#3}}} \def\nasequi#1#2#3{\aseqfromto{\uivar{#1}{#2}}{\uivar{#1}{#3}}} } \_@@_end_module: \endgroup % \end{macrocode} % % % \begin{macrocode} % % \end{macrocode} % % \end{implementation} % % \PrintIndex % \ifinfulldoc\else\printbibliography\fi % \endinput % Local Variables: % mode: doctex % TeX-master: t % End: