Skip to content
Snippets Groups Projects
Commit 0e14e021 authored by Hans-Jörg's avatar Hans-Jörg
Browse files

Add changes to changelog

parent 062a4959
No related branches found
No related tags found
1 merge request!5Document cvc5-style numerals
......@@ -33,7 +33,12 @@ Breaking changes:
only determined by its syntactic category.
\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.
Instead, the list of instatiation terms must follow the variable
order and cover all the respective bound variables.
\item Add new syntax for decimal and negative numbers and use it
for \proofRule{la_generic}.
\item Restrict sorting of numbers such that the sort of a constant is
only determined by its syntactic category.
\end{itemize}
\noindent
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment