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: Oct 13 2024 at 01:02 UTC