Re: [isabelle] Datatype definition can be slow
On Tue Apr 13, 2021 at 6:11 PM CEST, Manuel Eberl wrote:
> > "constructor_num x != constructor_num y ==> x != y"
> That works in this very simple case where your datatype is just an
> "enum"-like type. But in general, it should probably be something like
> "constructor_num x != constructor_num y ==> x a b c != y d e"
No, Dominique's statement works. For example, for "option", it could be
"constructor_num None = 0" |
"constructor_num (Some x) = 1"
This archive was generated by a fusion of
Pipermail (Mailman edition) and