evante.dev
When LLMs Try to Write Proofs
(Sub-)Types Are Not (Sub-)Sets
Dependently Typed Dates
Setting Up Idris for Development
Getting Into Quotients With Lean (3)
Some Basic Lattice Theory With Lean (2)
Getting Started With Lean (1)
Decidable Equality in Linear Lines
Coming to Idris2 from PureScript