Parsing and panic

Memoized Haskell-in-Lean

IO for linear algebra

Incorrect rects

Imperative Lean and Union-Find

Unsafe indexing and folds within folds

Folds! Monoids?

Custom syntax ∪ ranges

Fuel for the termination checker

Finding the batteries, learning to assert myself, and making a mess of number theory

Ranges, and treating numbers as strings

Learning the ropes again