When I run my example, I meet below hints:

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

I am curious about the principal behind this.

The part of snippet could be:

```
definition check_eqv :: "'a::order rexp ⇒ 'a rexp ⇒ 'a list ⇒ bool" where
"check_eqv r s as =
(let nr = norm r; ns = norm s
in case closure as (nr, ns) of
Some([],_) ⇒ True | _ ⇒ False)"
fun f :: "nat ⇒ bool" where
"f n = (n < 3)"
lemma "check_eqv (Plus One (Times ((Sym (Predicate.Pred f))) (Star (Sym (Predicate.Pred f))))) (Star(Sym (Predicate.Pred f))) [1,2,3,4]"
by eval
```

Any helps would be appreciated.

Well the error message basically says that the code generator is not able to generate code, because the only way is to enumerate all solutions…

how to improve such case

by looking at piece of the code, find out exactly which part is not working (I assume it is closure but I am not sure). Once you know that, you have to replace the code by something executable… (See https://isabelle.in.tum.de/dist/Isabelle2022/doc/codegen.pdf)

Hi, Mathisas. I thought I found the problem. I use the set comprehension to calculate the value.

Like`value "{a. f a}"`

But it is mandatory in my example I think.

like Mathias said, if you must use sets, you would have to provide rewrites for that in a more "executable" way that doesn't require searching over all numbers `a`

Last updated: Oct 12 2024 at 20:18 UTC