Hi all,

Is there some nice built-in support in Isabelle for converting a `nat`

to a ` char`

?

I am writing a function to enumerate all possible char values in isabelle:

```
fun all_chars :: "nat ⇒ char list"
where
"all_chars 0 = [char_of 0]"
|"all_chars (Suc i) = (char_of (Suc i)) # (all_chars i)"
```

I went through this answer

https://stackoverflow.com/questions/33393926/isabelle-character-and-string-literal-support

and somehow functions `nat_of_char`

and `char_of_nat`

wasn't there in the String.thy file.

I did find something called char_of, but somehow isabelle complains about it,

saying that

```
Additional type variable(s) in specification of "all_chars_graph": 'a
Extra type variables on rhs: "'a"
The error(s) above occurred in definition "all_chars_sumC_def":
"all_chars_sumC ≡ λx. THE_default undefined (all_chars_graph TYPE('a) x)"
```

How can I fix this? If I need to write one on my own, how should char_of_nat defined to be simple?

Thanks a lot,

Chengsong

```
fun all_chars :: "nat ⇒ char list"
where
"all_chars 0 = [CHR 0x00]"
|"all_chars (Suc i) = (char_of (Suc i)) # (all_chars i)"
```

Somehow this does the trick.

Can someone explain, please?

`of_char`

has the polymorphic type `'a => nat`

, thus in the expression `of_char 0`

the type of `0`

is also `'a`

(an additional type variable, that cannot be deduced from the function arguments). In the second equation (`Suc`

case), the type of `of_char`

can be specialized to `nat => char`

, as `Suc i`

has type `nat`

.

A simpler definition would be:

```
definition all_chars :: "nat ⇒ char list" where
"all_chars n = map char_of [0..n]"
```

Maximilian Schaeffeler said:

`of_char`

has the polymorphic type`'a => nat`

, thus in the expression`of_char 0`

the type of`0`

is also`'a`

(an additional type variable, that cannot be deduced from the function arguments). In the second equation (`Suc`

case), the type of`of_char`

can be specialized to`nat => char`

, as`Suc i`

has type`nat`

.A simpler definition would be:

`definition all_chars :: "nat ⇒ char list" where "all_chars n = map char_of [0..n]"`

Thanks a lot! That's a nice definition, except you need [0..n] needs n to be an int (which sounds weird to me as upto means "up to a positive number " right?

Chengsong Tan has marked this topic as resolved.

No, `n`

is of type `nat`

not `int`

in this definition.

There's also a version of this syntax that does not include `n`

:

```
definition "all_chars n = map char_of [0..<n]"
```

Last updated: Dec 07 2023 at 08:19 UTC