I was trying something like this

```

Definition genChar : G ascii :=

let start := nat_of_ascii "A" in

let end_ := nat_of_ascii "Z" in

let nats := (choose (start, end_)) in

let string_of_nat n := String (ascii_of_nat n) "" in

let str := fmap ascii_of_nat nats in

str.

```
Then write a function `G ascii -> G string` that fold all generated values for ascii to one string, but failing miserably
```

```
Definition genString : G string :=
fmap string_of_list_ascii (listOf genChar).
```

Thank you Li-yao. Every day I ask my self why I'm so terrible with Coq hahaha

Last updated: Feb 04 2023 at 22:29 UTC