Code related to the Lean verification of the empty hexagon theorem

Port of the haskell time library to Lean 4

Armv8 Native Code Symbolic Simulator in Lean

Enhancing the Factorio experience with SAT solvers

Google Scholar is a trans-exclusionary site. Don't use it. Help us demand change.

WIP collections library for Lean 4

bot for managing dependent PRs, particularly dependent PRs across GH projects

Leaff is a diff tool for Lean environments

Arbitrary Bit-Length Integers in Lean

some experiments with SMT-LIB

Basic HTTP definitions and parsing for Lean

A WIP definitional (co)datatype package for Lean4

A control flow graph library for Lean

Formalising the WASM spec in Lean

C0 specification and verified compiler in Lean

Reference compiler for c0

Efficient encoding for edge matching puzzles, to solve the Eternity II puzzle

A stepping debugger for Standard ML (SML)

MLB support for CM (the SML/NJ Compilation and Library Manager)

Standard ML of New Jersey

An example of how to use SML/NJ's Visible Compiler APIs

A language server for Standard ML.

Type-directed derived traits in SML

A custom parser/auto-formatter for Standard ML

🌲 Tree/Shrub data type visualization tool allowing conversion to-and-fro SML

A pure type system implemented in OCaml