Examples of Lean programs being verified in Lean

Stream: new members

[Ching-Tsun Chou]

Where can I find examples of Lean programs being verified in Lean? I am interested in both functional and imperative (namely, monadic) programs. This is for my own education, so simple (but not too simple) programs are what I'm looking for. Thanks in advance!

[pandaman]

Shameless plug:wink:

lean-regex is a verified regex engine implementation based on NFA compilation. Most of the code is written in functional style, but the core search logic is pretty much while loops disguised as pure functions. It's not super simple, but also not very big as a working program.

[Ching-Tsun Chou]

@pandaman Thanks for the pointer! This program is probably still much larger than my current state of knowledge can comprehend. What did you study when you were learning how to do it?

[pandaman]

Functional programming in Lean is a great resource to learn how to write programs in Lean and verify them

[Ching-Tsun Chou]

Thanks for the pointer!