Syntax reference

A dense reference for readers who already know what they are looking for. For explanation rather than recall, start at Values and types.

Comments

// Line comment.

/// Doc comment, attached to the next declaration.

Declarations

Functions

fn add(a: Nat, b: Nat) -> Nat { a + b }

fn identity<T>(x: T) -> T { x }        // generic

pub fn my_api(x: Nat) -> Nat { x + 1 } // exported

The last expression is the return value. return expr exits early.

Attributes on recursive functions

Since 2.0-alpha

type List = Nil | Cons(Nat, List)

#[decreasing(a)]                        // name the parameter that shrinks
fn zip_len(a: List, b: List) -> Nat {
    match a {
        Nil => 0,
        Cons(x, ra) => match b { Nil => 0, Cons(y, rb) => 1 + zip_len(ra, rb) },
    }
}

#[partial]                              // opt out of termination checking
fn halvings(n: Nat) -> Nat { if n < 2 { 0 } else { 1 + halvings(n / 2) } }

Every recursive function must be seen to stop; these are the two ways to tell the compiler more. See Recursion the compiler can see ends.

Theorems

theorem zero_eq_zero() -> Eq<Nat, 0, 0> {
    refl
}

Syntactically identical to fn; declares the signature to be a proposition.

Types

type Option<T> = None | Some(T)        // sum

type Shape =                            // sum, multi-line
    | Circle(Nat)
    | Rect(Nat, Nat)

type Pair<A, B> = MkPair(A, B)          // single constructor

type Point = { x: Nat, y: Nat }         // record

pub type Char = Nat                     // alias
pub type SourceEntry = (String, String)
pub type ParseResult<T> = Result<(T, Cursor), ParseError>   // generic alias

Extern functions

extern "C" fn tg_string_length(s: String) -> Nat

No body; binds to a C-ABI symbol at link time.

Let bindings

let x = 42;
let name: String = "hello";

let (a, b) = make_pair();          // tuple destructuring
let (x, (y, z)) = make_nested();   // nested
let (_, b) = make_pair();          // wildcard

let Some(n) = opt else { return 0 };   // let else; else must diverge

Modules

mod lexer;                 // expects lexer.tg or lexer/mod.tg
pub mod math;

use lexer::token::Token;
use driver::{parse_args, dispatch_command};
use util::original_name as renamed;    // aliasing

Paths are absolute from the crate root; there is no super. Declarations are private unless marked pub.

Types

Built-in

Compound

(Nat, Nat)              // tuple
(Nat) -> Nat            // function
A -> B                  // function, single argument
Option<Nat>             // generic instantiation
Eq<Nat, 0, 0>           // propositional equality

Expressions

Literals

42  -7  true  false  "hello"  ()  (1, 2)

42 is a Nat unless the context asks for an Int; -7 is an Int.

Operators

if

let label = if count == 1 { "item" } else { "items" };

if n == 0 { "empty" } else if n < 10 { "small" } else { "large" }

An expression; both branches must have the same type.

match

match opt {
    None() => "nothing",
    Some(n) => "got one",
}

match o {
    Some(Some(n)) => n,        // nested patterns
    Some(None()) => 1,
    None() => 0,
}

match parsed {
    Ok((token, cursor)) => token,   // tuple inside constructor
    Err(e) => fallback,
}

Exhaustiveness is checked.

if let

if let Some(n) = maybe { n + 1 } else { 0 }

if let Ok(x) = a && let Ok(y) = b { x + y } else { 0 }   // chained

Lambdas

let inc = |x: Nat| x + 1;
let add = |a: Nat, b: Nat| a + b;
let step = fn(k: Nat, acc: Nat) => acc;   // alternative spelling

Records

let p: Point = { x: 0, y: 10 };     // construction
let q = Point { x: 0, y: 10 };      // named constructor
let r: Point = { ...p, x: 5 };      // spread; needs the annotation
let v = p.x;                        // field access

Error handling

let x = parse(a)?;                  // early return on failure

let r: Result<Nat, String> = try {  // annotation required
    let x = parse(a)?;
    x + 1                           // body yields T; try wraps in Ok
};

Blocks

let result = {
    let (x, y) = make_pair();
    x + y
};

Proof terms

refl                                  // proof that x = x
sym(p)                                // flips an equality proof
trans(p, q)                           // chains two equality proofs
cong(f, p)                            // congruence
subst(a, b, c)                        // substitution / rewriting
natind(motive, base, step, n)         // induction over naturals
natrec(type, base, step, n)           // primitive recursion

Note refl is lower-case. See Induction over naturals for worked uses of natind.

Patterns

A match on a number needs exactly one catch-all arm without a guard.

Entry point

fn main() -> String { "hello world" }

fn main() -> Nat { 42 }

The result is printed; the process exits 0.

Semicolons

let bindings end with ;. The final expression of a block does not. Match arms are separated by ,.

fn example() -> Nat {
    let x = 1;
    let y = 2;
    x + y
}

Not supported

These are the things a Rust or Lean reader is most likely to reach for and not find. See Current limitations for the full list with detail.

• Turbofish — identity::<Nat>(42) does not parse. Annotate instead.
• String interpolation — "{name}" is literal braces. Use ++.
• Tuple index access — no p.0. Destructure instead.
• let mut — planned for v2.0.
• Or-patterns on constructors — A() | B() => ... is planned for v2.0. On numbers they work.