lean2ts
Converts Lean 4 specs into TypeScript types, function stubs and fast-check property tests.
What it does
- Types from structure and inductive
- Theorems become fast-check property tests
- Function stubs generated from def
Families
Writing in other languages
Written outside my own language: lean2ts turns Lean 4 theorems into TypeScript property tests, lean4-rust-backend lowers Lean to Rust, and before either of those comes the practice (hello-lean4, lean-lang-sandbox, lean4-practice, fizzbuzz-lean4-lib, fizzbuzz-lean4-cli); zfp is a zero-cost functional toolkit that disappears into Zig's types; sashiko watches Ruby's concurrency boundaries through OpenTelemetry; archgopher, in Go, pushes the expected load through a Terraform architecture and reads its cost and headroom.
All families10
Repositories
284
Commits
6
Languages
2026–2026
Span
One in full
Work
10 / 10-
lean2ts O6lvl4
Converts Lean 4 specs into TypeScript types, function stubs and fast-check property tests.
- Lean
- code-generation
- fast-check
-
zfp O6lvl4
Zero-cost functional programming toolkit for Zig, working directly on native ?T and E!T
- functional-programming
- maybe
- option
-
sashiko O6lvl4
Ruby library that keeps OpenTelemetry traces connected across Thread, Fiber, queue and Ractor boundaries.
- concurrency
- distributed-tracing
- observability
-
archgopher O6lvl4
Read an architecture before you build it: push the expected load through Terraform and read cost, headroom, latency and availability
- TypeScript
- CSS
-
hello-lean4 O6lvl4
A Hello World CLI app written in Lean 4, with prebuilt binaries for Linux and macOS.
-
lean-lang-sandbox O6lvl4
Lean 4 learning sandbox with ten step-by-step tutorials, from theorem proving to programming
- functional-programming
- japanese
- lean
-
fizzbuzz-lean4-cli O6lvl4
A FizzBuzz command-line app written in Lean 4, built on fizzbuzz-lean4-lib
-
lean4-rust-backend O6lvl4
A Lean 4 to Rust backend that generates Rust code from Lean's IR, with a runtime and WASM support.
- Lean
-
lean4-practice O6lvl4
A Claude Code plugin providing best practices for generating Lean 4 code.
-
fizzbuzz-lean4-lib O6lvl4
A FizzBuzz library written in Lean 4, usable as a Lake dependency.