Re: [isabelle] Datatype definition can be slow




No, Dominique's statement works. For example, for "option", it could be
defined as

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

Yes, that's what I had in mind.

Best wishes,
Dominique.






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