Skip to content
Snippets Groups Projects

Document cvc5-style numerals

Merged Hans-Jörg requested to merge devel/decimals into master
All threads resolved!
1 file
+ 6
1
Compare changes
  • Side-by-side
  • Inline
+ 6
1
@@ -33,7 +33,12 @@ Breaking changes:
@@ -33,7 +33,12 @@ Breaking changes:
only determined by its syntactic category.
only determined by its syntactic category.
\item The arguments for \proofRule{forall_inst} have been changed to
\item The arguments for \proofRule{forall_inst} have been changed to
no longer take the shape of bindings using \texttt{(:= x c)}.
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}
\end{itemize}
\noindent
\noindent
Loading