[isabelle] No type arity nat :: equal



Dear Code generation experts,

I get this error

Wellsortedness error:
Type nat not of sort {equal,order}
No type arity nat :: equal

What do I need to do?

In a bit more detail: I have generalised the Regular-Sets AFP entry by replacing
nat by 'a::order. This results in the above error when executing the proof
method regexp. The latter intentionally still uses nat, but I expected the class
system to take care of that.

Thanks in advance!
Tobias




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