edouard.paris
Verify Gleam functions in Lean 4.
Update README
author
edouardparis
date
(Jul 24, 2026, 10:15 AM +0200)
commit
0a7e31f4
0a7e31f46aaea76ebd4323b16f92899d61714912
parent
e72e8fe0
e72e8fe0a1e468c8b4307e049f5494a1b35c1ca3
change-id
krozqryr
krozqryrksmoyzoyxkzvtlnpwutyuvyl
+27
-17
+27
-17
README.md
+27
-17
README.md
···
1
1
# Glean
2
2
3
-
Verify Gleam functions in Lean 4. `glean` translates the functions you mark with
3
+
Verify [Gleam](https://gleam.run) functions in [Lean 4](https://lean-lang.org/).
4
+
5
+
`glean` translates the functions you mark with
4
6
a `/// @proof` doc comment into Lean 4 definitions (via
5
7
[hax](https://github.com/cryspen/hax)), so you can prove properties about them.
6
8
7
9
Requires [Nix](https://nixos.org) with flakes. The engine is currently bundled.
8
10
9
-
## Setup
11
+
## Nix Setup
10
12
11
13
Add glean to your project's `flake.nix` so `glean` is on your `PATH`:
12
14
···
56
58
## 3. Extract
57
59
58
60
```sh
59
-
glean prove src/fibonacci.gleam
61
+
glean prove
60
62
```
61
63
62
-
This writes two files under `proofs/lean/Proofs/`:
64
+
With no argument, `glean prove` extracts every `@proof`-marked module under your
65
+
project's `src/`. Under `proofs/lean/Proofs/` it writes, per module:
63
66
64
67
- `fibonacci.lean`: the generated Lean definitions. **Do not edit**; glean
65
68
regenerates it each run. Gleam `Int` is modeled as Lean's arbitrary-precision
66
69
`Int` (as `gleam.Int`), so proofs reason about true integers, not fixed-width
67
-
ones. glean injects a small prelude mapping the Gleam operators onto it. For the
68
-
`fib` above it contains:
70
+
ones. The file imports the shared model library (below); for the `fib` above it
71
+
is:
69
72
70
73
```lean
71
74
import Hax
72
-
-- (opens and set_options elided)
73
-
74
-
namespace gleam
75
-
abbrev Int := _root_.Int
76
-
end gleam
77
-
78
-
namespace gleam.int
79
-
def add (a : gleam.Int) (b : gleam.Int) : RustM gleam.Int := pure (a + b)
80
-
def sub (a : gleam.Int) (b : gleam.Int) : RustM gleam.Int := pure (a - b)
81
-
-- (mul, div, comparisons, … elided)
82
-
end gleam.int
75
+
import Proofs.GleamModels
76
+
-- (Std.Do imports, opens, and set_options elided)
83
77
84
78
namespace fibonacci
85
79
···
95
89
partial_fixpoint
96
90
97
91
end fibonacci
92
+
```
93
+
94
+
- `GleamModels.lean`: a shared library, regenerated each run and imported by every
95
+
generated module, mapping Gleam types and operators onto Lean. It defines
96
+
`gleam.Int` and the arithmetic the code above calls:
97
+
98
+
```lean
99
+
namespace gleam
100
+
abbrev Int := _root_.Int
101
+
end gleam
102
+
103
+
namespace gleam.int
104
+
def add (a : gleam.Int) (b : gleam.Int) : RustM gleam.Int := pure (a + b)
105
+
def sub (a : gleam.Int) (b : gleam.Int) : RustM gleam.Int := pure (a - b)
106
+
-- (mul, div, comparisons, … elided)
107
+
end gleam.int
98
108
```
99
109
100
110
- `fibonacciProofs.lean`: a stub for **your** theorems. glean creates it once and