Add Proof Environment

This commit is contained in:
JanUlrich 2024-06-11 12:00:41 +02:00
parent d4040b2611
commit 5fc1972c41

View File

@ -23,6 +23,8 @@
\usepackage{mathpartir}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{enumitem}
%\usepackage{amsthm}
\begin{document}
%
@ -230,4 +232,29 @@ constraints in the original constraint set and
there exists a typing for the remaining type placeholders
so that the constraint set is satisfied.
Proof:
\SetEnumitemKey{ncases}{itemindent=!,before=\let\makelabel\ncasesmakelabel}
\newcommand*\ncasesmakelabel[1]{Case #1}
\newenvironment{subproof}
{\def\proofname{Subproof}%
\def\qedsymbol{$\triangleleft$}%
\proof}
{\endproof}
\begin{proof}
Some text or \texttt{\string\leavevmode} (so the enumerate starts in another line)
\begin{enumerate}[ncases]
\item $\tv{a} \lessdot \type{T}$ where $\tv{a} \notin \type{T}$.
\begin{subproof}
Lorem ipsum dolor sit amet, consectetur adipisicing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.
\end{subproof}
\item Bar.
\begin{subproof}
Lorem ipsum dolor sit amet, consectetur adipisicing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.
\end{subproof}
\end{enumerate}
And more text.
\end{proof}
\end{document}