## Stream: Beginner Questions

### Topic: About the code generation- Wellsortedness error

#### Hongjian Jiang (Jul 27 2023 at 13:47):

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.

#### Mathias Fleury (Jul 27 2023 at 13:50):

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…

#### Hongjian Jiang (Jul 27 2023 at 13:51):

how to improve such case

#### Mathias Fleury (Jul 27 2023 at 13:55):

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)

#### Hongjian Jiang (Jul 28 2023 at 13:45):

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

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

#### Hongjian Jiang (Jul 28 2023 at 13:46):

But it is mandatory in my example I think.

#### Yong Kiam (Jul 31 2023 at 00:57):

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: Dec 07 2023 at 20:16 UTC