syntaxAlchemist/ladder-calculus
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

paper: add new coq files to appendix

Browse source
This commit is contained in:
Michael Sippel 2024-09-04 12:44:24 +02:00
parent b31c8abc6c
commit fd8ca35a27
Signed by: senvas
GPG key ID: F96CF119C34B64A6
1 changed files with 12 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
paper/appendix.tex
View file

@ -20,11 +20,23 @@ This document lists the Coq-Sourcecode from commit
\label{coq:equiv} \label{coq:equiv}
\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/equiv.v} \inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/equiv.v}
\subsection{subtype.v}
\label{coq:typing}
\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/subtype.v}
\subsection{typing.v} \subsection{typing.v}
\label{coq:typing} \label{coq:typing}
\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/typing.v} \inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/typing.v}
\subsection{morph.v}
\label{coq:typing}
\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/morph.v}
\subsection{smallstep.v} \subsection{smallstep.v}
\label{coq:smallstep} \label{coq:smallstep}
\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/smallstep.v} \inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/smallstep.v}
\subsection{soundness.v}
\label{coq:smallstep}
\inputminted[fontsize=\footnotesize, linenos, mathescape]{coq}{../coq/soundness.v}