Stream: Coq users

Topic: How to generate a random string for QuickChick?

Daniel Hilst Selli (Jan 06 2022 at 19:48):

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

Li-yao (Jan 06 2022 at 19:55):

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

Daniel Hilst Selli (Jan 06 2022 at 19:56):

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

Last updated: Apr 19 2024 at 15:02 UTC