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
defined as

"constructor_num None = 0" |
"constructor_num (Some x) = 1"

Regards,
Jakub Kądziołka




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.