Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] No type arity nat :: equal

Email Gateway (Aug 19 2022 at 12:03):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>

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.

A rough guess: when

definition
check_eqv :: "nat rexp \<Rightarrow> nat rexp \<Rightarrow> bool" …

is generalized to

definition
check_eqv :: "'a::order rexp \<Rightarrow> 'a::order rexp
\<Rightarrow> bool" …

the instance nat :: equal is not present in the transitive closure of
code equations specified in

val regexp_conv = Code_Runtime.static_holds_conv thy
[@{const_name Zero}, @{const_name One}, @{const_name Atom}, @{const_name Plus},
@{const_name Times}, @{const_name Star},
@{const_name check_eqv}, @{const_name Trueprop}]

This is easiest resolve by defining a separate

definition check_eqv :: "nat rexp \<Rightarrow> nat rexp \<Rightarrow>
bool" …
where
"check_eqv = Equivalence_Checking.check_eqv"

in Regexp_Method.thy and using this in the the definition of regexp_conv
(which in this case means not to change the text of this definition).

Hope this helps,
Florian
signature.asc

Email Gateway (Aug 19 2022 at 12:20):

From: Tobias Nipkow <nipkow@in.tum.de>
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

Last updated: Nov 21 2024 at 12:39 UTC