Menu
▾
▴
#36 ConstDecl paragraphs don't have 'box' type changed
Using the unfolding rules, the following paragraph:
\begin{zed}
x == 1
\end{zed}
is rewritten to:
\begin{zed}
x : \arithmos
\where
x = 1
\end{zed}
Which is correct, except this should be an axdef. This seems like something that would have to be explicitly dealt with in the prover -- I don't think a rule could deal with it?
Logged In: YES
user_id=810607
Originator: NO
Currently, the prover is designed to work for predicates, expressions, and schema texts only. It isn't supposed to be used for a whole specification or paragraph so I guess the best solution is to properly document that and then close this bug.