Skip to content
Snippets Groups Projects

Update forall_inst

Merged Hans-Jörg requested to merge devel/new-forall_inst into master
+ 3
0
@@ -16,6 +16,9 @@ Breaking changes:
\item Add the sort to all variables in contexts. Before, the context
of a bind could be \texttt{(x S) (:= y x)}. Now it must
be \texttt{(x S) (:= (y S) x)}.
\item The arguments for \proofRule{forall_inst} have been changed to
no longer take the shape of bindings using \texttt{(:= x c)}.
Instead, the list of instatiation terms must follow the variable order and cover all the respective bound variables.
\end{itemize}
\noindent
Loading