lean2ts
Lean 4の仕様をTypeScriptの型・スタブ・fast-checkテストへ変換するツール
できること
- structure/inductiveから型を生成
- theoremをfast-checkの性質テストへ変換
- defから関数スタブを生成
系統
他の言語で書く
自作言語の外で書いたもの。Lean 4 の定理を TypeScript のプロパティテストに落とすもの（lean2ts）、Lean を Rust に落とすバックエンド（lean4-rust-backend）、その手前の証明の練習（hello-lean4・lean-lang-sandbox・lean4-practice・fizzbuzz-lean4-lib・fizzbuzz-lean4-cli）、Zig の型で消えるゼロコスト関数型ツールキット（zfp）、Ruby の並行境界を OpenTelemetry で覗くもの（sashiko）、Terraform の構成に負荷を流して費用と余力を読む Go の道具（archgopher）。
系統の一覧へ10
公開リポジトリ
284
コミット
6
言語
2026–2026
期間
代表作
つくったもの
10 / 10-
lean2ts O6lvl4
Lean 4の仕様をTypeScriptの型・スタブ・fast-checkテストへ変換するツール
- Lean
- code-generation
- fast-check
-
zfp O6lvl4
Zigのネイティブ型上で動くゼロコストの関数型ツールキット
- functional-programming
- maybe
- option
-
sashiko O6lvl4
OpenTelemetry上でRubyの並行処理境界をまたいでトレースをつなぐ可観測性ライブラリ
- concurrency
- distributed-tracing
- observability
-
archgopher O6lvl4
つくる前に構成を読む。Terraform に想定の負荷を流し、費用・余力・遅延・可用性を見積もる
- TypeScript
- CSS
-
hello-lean4 O6lvl4
Lean 4 で書かれた Hello World CLI アプリ
-
lean-lang-sandbox O6lvl4
定理証明からプログラミングまで学べるLean 4のチュートリアル集
- functional-programming
- japanese
- lean
-
fizzbuzz-lean4-cli O6lvl4
Lean 4 製の FizzBuzz CLI。fizzbuzz-lean4-lib を利用する
-
lean4-rust-backend O6lvl4
Lean 4をRustへ変換するIRベースのコード生成バックエンド
- Lean
-
lean4-practice O6lvl4
Lean 4コード生成のベストプラクティスを提供するClaude Codeプラグイン
-
fizzbuzz-lean4-lib O6lvl4
Lean 4 で書かれた FizzBuzz ライブラリ