lean2ts
将Lean 4规约转换为TypeScript类型与属性测试
功能
- 由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），用 OpenTelemetry 看 Ruby 并发边界的 sashiko，以及把预期负载灌进 Terraform 架构、读出成本与余量的 Go 工具 archgopher
全部系列10
公开仓库
284
提交
6
语言
2026–2026
年份
详看一件
作品
10 / 10-
lean2ts O6lvl4
将Lean 4规约转换为TypeScript类型与属性测试
- Lean
- code-generation
- fast-check
-
zfp O6lvl4
基于Zig原生类型的零开销函数式工具库
- functional-programming
- maybe
- option
-
sashiko O6lvl4
跨Ruby并发边界保持OpenTelemetry链路连续的库
- 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 命令行程序
-
lean4-rust-backend O6lvl4
基于IR的Lean 4到Rust代码生成后端
- Lean
-
lean4-practice O6lvl4
提供Lean 4代码生成最佳实践的Claude Code插件
-
fizzbuzz-lean4-lib O6lvl4
用 Lean 4 编写的 FizzBuzz 库