Guillaume Verdier
-
2020-11-30
- Milestone: Rodin 3.1 --> Later
In the attached example, a Stack datatype is defined inductively:
STACK(S) = EmptyStack |
Push(top:S, rest: STACK(S))
An operator top(s : STACK) is defined with well-definedness condition "s != EmptyStack)
top is defined recursively
top(Push(t,r)) = t
However, an error is "Not all inductive cases are covered" for the theory.
This is too restrictive since the well-definedness condition guarantees that all cases are covered for any well-defined input.
Son