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

Remove confusing sentence fragment

parent eaeb3951
No related branches found
No related tags found
1 merge request!5Document cvc5-style numerals
......@@ -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
......
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