Lists (32)
📽 Animation
5 repositories
🖼️ Art
3 repositories
📜 Binary Formats
54 repositories
🌀 Bootstrapping
49 repositories
🏗️ Build systems
13 repositories
📝 Compilation
32 repositories
🎨 Creative Tools
38 repositories
🗄 Data Layout
3 repositories
🌱 Digital Gardens - Examples
10 repositories
🌱 Digital Gardens - Tools
42 repositories
📖 Documentation - Tools
3 repositories
🚀 Effects
Effect systems, Algebraic effects and handlers… resources, languages, libraries and use cases56 repositories
🗣 Elaboration
Examples of elaborating surface languages into minimal core languages26 repositories
🐟 Fish Shell
4 repositories
🔠 Fonts
28 repositories
🕹️ Game Development
3 repositories
🕹️ Games
2 repositories
📐 Geometric Algebra
18 repositories
👍 Memory Safe by Default
4 repositories
🍱 Module Systems - Case Studies
3 repositories
🍱 Module Systems - Languages
12 repositories
🏡 My Stack
14 repositories
⚙️ Nix - Example Configurations
12 repositories
⚙️ Nix - Tools
37 repositories
💾 Nostalgia
29 repositories
🐪 OCaml - js_of_ocaml
3 repositories
🏔 Procedural
Things related to procedural generation, generated worlds, etc.57 repositories
🎲 Property Based Testing
4 repositories
🖼 Shaders
16 repositories
⏱ Staged Programming
8 repositories
🌳 Structural Editing
14 repositories
🏔 World Building - Conlanging
8 repositories
Starred repositories
64
stars
written in Lean
Clear filter
Lean 4 programming language and theorem prover
Lean 3's obsolete mathematical components library: please use mathlib4
Demo for high-performance type theory elaboration
Tactics for discharging Lean goals into SMT solvers.
A verifier for automated and interactive proofs about transition systems.
Lean 4 kernel / 'external checker' written in Lean 4
Lean 4 port of Iris, a higher-order concurrent separation logic framework
Experiments on automation for Lean
A formal proof of the independence of the continuum hypothesis
Perfectoid spaces in the Lean formal theorem prover.
Natural language tactics to teach mathematics using Lean 4
A Lean tactic for Canonical, a search procedure for terms in dependent type theory.
A Lean 4 library for configuring Command Line Interfaces and parsing command line arguments.
**(Deprecated: Merged into Lean 4)** Lean 4 build system and package manager with configuration files written in Lean.
Canonical is a performant sound and complete type inhabitation solver for dependent type theory.
tool for turning Lean proofs into Blender animations
A formal consistency proof of Quine's set theory New Foundations