Stream: Coq users

Topic: How to generate a random string for QuickChick?


view this post on Zulip 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

view this post on Zulip Li-yao (Jan 06 2022 at 19:55):

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

view this post on Zulip 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: Feb 04 2023 at 22:29 UTC