Property-based testing

Stream: general

[Daniel Fabian]

Has anyone here seen a way to do property-based testing a la QuickCheck for lean here? I'd like my parser to round-trip and doing the full formal proof turns out to be quite tedious (combining strings, monadic parsing and recursive AST with a list node as this needs special induction).

[Johan Commelin]

There is a PR, I think

[Markus Himmel]

#2080

[Daniel Fabian]

cool, thx!