Unsupported algebraic datatypes error with alt-ergo
The following type definition causes an error from Alt-Ergo:
type omg 'a = Omg
Error message:
internal failure: This declaration isn't supported:
type omg 'a =
| Omg
alt-ergo: algebraic datatype are not supported
On the other hand, code using this same definition works perfectly in other provers like z3 (for which why3 doesn't use ADTs).