GitHub repository: tydeu/imperia
Primary language: Lean
Description: Experimenting with imperative programming in Lean