Re: [isabelle] Datatype definition can be slow



Ah, okay, I misunderstood. Yes, I suppose that should work. Might indeed
be the easiest and fastest way to do it.

Nice idea!

Manuel


On 13/04/2021 18:13, Jakub Kądziołka wrote:
> 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
> 

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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