Numerical packages in lean numlean lean karray

Webserver example. Custom syntax

novice friendly induction tactic

metaprogramming framework for formal verification lean4

“The Lean typeclass resolution procedure can be viewed as a simple λ-Prolog interpreter [8], where the Horn clauses are the user declared instances.” That sounds fun


elan tool


lake is a new build tool on the horizon

Using nix is kind of a pain. I haven’t done it.