Skip to content
Snippets Groups Projects

Document cvc5-style numerals

Merged Document cvc5-style numerals
devel/decimals into master
All threads resolved!
Merged Hans-Jörg requested to merge devel/decimals into master
All threads resolved!
Viewing commit ebfd3b93
Prev Next
Show latest version
1 file
+ 1
− 2
Compare changes
  • Side-by-side
  • Inline
spec/doc.tex
+ 1
− 2
@@ -832,8 +832,7 @@ is always \inlineAlethe{Int}.
For example, in standard {\smtlib}, the term \inlineAlethe{(+ 5 3)}
has the sort \inlineAlethe{Int} in the logic \texttt{QF\_LIA}, but
has the sort \inlineAlethe{Real} in \texttt{QF\_LRA}.
In Alethe, this term always has the sort \inlineAlethe{Int},
and would not be well sorted in the logic \texttt{QF\_LRA}.
In Alethe, this term always has the sort \inlineAlethe{Int}.
\paragraph{Subproofs}
The abstract notation denotes subproofs by marking them with a vertical