TinyLean

Tiny theorem prover in Python, with syntax like Lean 4.

Tour

An identity function in TinyLean:

def id {T: Type} (a: T): T := a

example := id Type

Inductive data types:

inductive Maybe (A: Type) where
| Nothing
| Just (a: A)
open Maybe

inductive N where
| Z
| S (n: N)
open N

inductive Vec (A: Type) (n: N) where
| Nil (n := Z)
| Cons {m: N} (a: A) (v: Vec A m) (n := S m)
open Vec

The typechecker knows if any case is impossible (i.e. dependent pattern matching):

def v0: Vec N Z := Nil

example :=
  match v0 with
  | Nil => Z
  /- Cons is impossible, leaving it here yields errors. -/

So a bottom type eliminator is trivial via DPM:

inductive Weird (n: N) where
| MkWeird (n := Z)
open Weird

/- Impossible to construct a term for type `Weird (S Z)`. -/
example {A: Type} (x: Weird (S Z)): A := nomatch x

License

MIT