Playground

Everything here runs in your browser — the compiler is compiled to WebAssembly and loaded on your first click, so nothing you write is sent anywhere. Pick a starting point, edit it, and press Check or Run.

Compiled with Albite 2.0.0-beta

// An ordinary function.
fn add(a: Nat, b: Nat) -> Nat {
    a + b
}

// A proposition, and its proof. Eq<T, a, b> is the claim that a
// equals b at type T; refl proves it when both sides compute to
// the same value. Checked at compile time, by the same pass.
theorem two_plus_two_is_four() -> Eq<Nat, 2 + 2, 4> {
    refl
}