fibonacci — a glean proof example#

A small, real Gleam project used to exercise glean end-to-end: it marks functions with /// @proof and extracts them to Lean via glean prove.

src/fibonacci.gleam proves:

• fib_loop — the tail-recursive core (pure Int recursion).
• fib — the nth Fibonacci number as Result(Int, Nil) (Nil lowers to Lean Unit).
• fib_option / fib_or_zero / fib_doubled — over gleam/option, lowering the project's real gleam_stdlib option.unwrap / option.map (not a vendored model).

Running it#

glean resolves imports from the project's built dependencies, so build first — the build/ directory is git-ignored and must be regenerated on a fresh checkout:

gleam build                                   # fetch + compile deps (once)
glean prove src/fibonacci.gleam --stdout      # extract the @proof functions to Lean

The project must be built with the gleam version glean embeds (see the repo's flake shell hook); a mismatch is reported by glean prove.