Cella language reference

This document describes every construct of Cella: how to write it and what it means. You can try it in the editor at cella-lang.org.

Every cella code block below is a complete file that can be checked.

1. Files and modules

A file is a module. The modules it uses come first, then the declarations.

import std
import io
import string

def main : IO Unit := putStr "hello"

• import M: use the public definitions of module M.
• import M as N: refer to them as N.name.
• import M (a, b): take only a and b.
• import can only come before the first declaration.
• A module name can contain dots, and a dot is a directory:
  • import util.math is util/math.cella next to the entry file;
  • import cpp.int is the submodule packages/cpp/src/int.cella of the package cpp.
• A library definition (the standard library and the packages) is named by its namespace only, whatever file it is in: add under namespace cpp in cpp.int is cpp.add. A program’s definitions carry the module name (util.math.m).
• Common modules: std (natural numbers, booleans, lists, paths and other basics), io (input and output, and IO), string (string operations), int (integers), notation (infix notation such as +).

2. Lexical structure

Symbols are ASCII first, each with an easy-to-type spelling; the Unicode spellings are aliases: -> (→), <- (←), * (×), Path a b (a ≡ b), /\ (∧), \/ (∨). Error messages and Inspect print ASCII by default (pass --unicode on the command line, or call set_unicode_output(true) in the browser, to print Unicode).

2.1 Comments

import std
-- a line comment
/- a block comment,
   /- which can nest -/ -/
/-- a documentation comment: attached to the next declaration -/
def one : Nat := 1

2.2 Names

• A name starts with a letter (any Unicode letter, including Chinese and Greek) or _, followed by letters, digits, _ and ': x, x', α₁, succ_lemma.
• Qualified names are joined with .: Nat.add, p.x.
• A lone _ is a hole (a part for Cella to infer), not a name.
• Escaping: r#name is the identifier called “name”, which can be a keyword or _: def r#in (r#data : Nat) : Nat := r#data, fun (r#_ : Nat) => r#_. The part after a dot can be a keyword as it is: v.end, Vector.end (defined inside a namespace as def r#end). Messages print a name that is a keyword as r#name. The keywords are listed in the appendix.

2.3 Numbers

Decimal natural numbers: 0, 42, 18446744073709551616 (big numbers too). In a negative number -3, the - must touch the digits.

2.4 Strings

import std
import string

def plain : String := "an ordinary string, escapes \n \t \" \\"
def name : String := "Cella"
def greeting : String := f"hello, {name}! {{the braces themselves}}"
def poem : String := """
  the first line
  the second line
  """
def raw : String := r"""
  printf("%d\n", x);
  """

• "…": an ordinary string, on one line; the only escapes are \n \t \r \" \\.
• f"…{e}…": string interpolation. The expression in {e} is turned into a string with ToString; {{ and }} are the braces themselves.
• """…""": a multi-line string. The indentation is removed up to the column of the closing """; the line break right after the opening """ does not count.
• f"""…""": a multi-line string with interpolation.
• r"""…""", fr"""…""": backslashes are not escapes (good for embedding another language’s source).

3. Declarations

Every declaration starts with a keyword, followed by the name, the parameters and the type.

3.1 def and theorem

import std

def double (n : Nat) : Nat := add n n

theorem doubleZero : double 0 ≡ 0 := refl

• def name parameters… : type := body. The type must be written.
• theorem is written like def, for proofs.
• The body can be followed by a where clause, defining helpers used only in this definition (see below).

data Nat = zero | succ Nat
data Bool = true | false

def isEven (n : Nat) : Bool := ev n
  where
    ev (k : Nat) : Bool := match k with
      | zero => true
      | succ j => od j
    od (k : Nat) : Bool := match k with
      | zero => false
      | succ j => ev j

def count (start : Nat) (n : Nat) : Nat := go n
  where go (k : Nat) : Nat := match k with
    | zero => start
    | succ j => succ (go j)

• A where clause is name parameters… : type := body. When the clause names start their lines, the next name in the same column is the next clause; on the same line as where, clauses are separated by ;. A clause can have its own where.
• Clauses can recurse, call each other and call outer definitions; they can use the outer definition’s parameters (start in count).
• A clause is a top-level definition of its own, outer.clause (count.go), whose parameters are the outer parameters it uses plus its own; its termination is checked like any definition’s. A clause without a type can only be non-recursive.

Proving termination with a measure

A recursive definition must decrease structurally by default (recursing on subterms of a parameter; lexicographic orders and mutual recursion are found automatically). When it does not recurse on a subterm, write termination_by measure after the body:

import omega

def upto (n : Nat) (m : Nat) : Nat :=
  if Nat.blt n m then upto (succ n) m else n
termination_by sub m n

• The measure is a Nat and can use the parameters. Each recursive call must make it smaller: the measure at the call’s arguments is smaller than the measure at the current parameters.
• The proof sees the conditions of the enclosing ifs and what a match learned about the parameters. It is proved with omega by default (which needs import omega); omega knows addition, multiplication by constants, truncated subtraction sub and pred.
• When it cannot be proved, the error says which call, with the measures on both sides. You can prove it yourself with decreasing_by { tactics } after termination_by: the goal is “the measure at the call < the bound”, and the context has “the current measure < the bound + 1” and the if conditions.
• In mutual recursion (mutual), every definition needs a measure.
• A recursive name can only appear as a call with all its explicit arguments: it cannot be passed to map as a function, or appear in a do or tactic block.
• The definition becomes a version with a bound, name.bounded: the bound starts at “measure + 1” and decreases by one at each recursive call, so it computes as usual (refl, and all three backends of cella run), and the measure is computed once, at the entry. Unfolding name in a proof shows this version first.

3.2 Parameters

import std

def const {A : Type} {B : Type} (a : A) (b : B) : A := a

def pick (b : Bool) (x y : Nat) : Nat := match b with
  | true => x
  | false => y

• (x : A): an ordinary parameter; (x y : A) declares several parameters of one type.
• {A : Type}: an implicit parameter, inferred by Cella at the call; to give it explicitly write f {Nat} x.
• {{inst : C A}}: an instance parameter, filled by type class instance resolution.
• (0 x : A): an erased parameter (used only in types, absent at run time); (1 x : A): a linear parameter (used exactly once).
• A mode can allow other usages: mode X extends core grades {0, omega} (omega, or ω, is any number of times), or a semiring of your own (see Type theories).

3.3 postulate

postulate name parameters… : type: declares a constant without a definition (an assumption). The verdict of a definition that uses it lists this assumption.

extern name parameters… : IO (Either String result): declares a function provided by the running environment (an external function). Type checking treats it as a postulate; the verdict lists it as an “external function” assumption (kind is external in the JSON), on every definition that uses it, directly or not.

import std
import io

extern host_write (port : Nat) (level : Nat) : IO (Either String Unit)

def signal : IO (Either String Unit) := host_write 2 1

• The parameters can only be Nat or Bool, and must be explicit (not implicit parameters); the result is always an IO that can fail, and result is Nat, Bool or Unit.

• The type can be followed by ensures p (p : result -> Bool): the caller gets an IO.Ensured result p, which on success carries a proof of p v = true that can be used directly. When the value the host returns does not pass p, the program gets left, with a message saying it broke the contract; this is a run-time check, not an axiom.

  import std
  import io
  
  extern host_level (port : Nat) : IO (Either String Nat) ensures (fun (v : Nat) => Nat.blt v 2)

• Cella has no built-in external functions. Which functions exist is declared by the environment’s own package; in an environment that does not provide one, the call gets left, with a message saying it is not provided, and the program can handle it.

• For a program compiled to a WebAssembly component, an external function’s place in a WIT interface is written @[wit "interface" "signature"], and a definition marked @[wit "run: func()"] is one of the component’s exports. The WIT signature is the source of truth: parameters one to one, in order, u8, u16, u32, u64 for Nat, bool for Bool, string for String, no result for IO Unit; a mismatch is refused, naming the parameter. This version takes one interface and functions without results, and exports only IO Unit without parameters. At run time a Nat past its WIT type’s width stops the run.

  import std
  import io
  
  @[wit "cos-mos:device/device@0.1.0" "pin-write: func(pin: u8, level: bool)"]
  extern pinWrite (pin : Nat) (level : Bool) : IO Unit
  
  @[wit "run: func()"]
  def run : IO Unit := pinWrite 2 true

3.4 data (inductive types)

import std

data Color = red | green | blue

data Tree (A : Type) = leaf | node (Tree A) A (Tree A)

def size {A : Type} (t : Tree A) : Nat := match t with
  | leaf => 0
  | node l x r => succ (add (size l) (size r))

• data name parameters… = constructor | constructor | …; an extra | can come before the first constructor.
• A constructor is written name argument-types…, or name : full type, or name (x : A) … : result type.
• An indexed type: data Vec (A : Type) : Nat -> Type = ….
• deriving C1, C2 at the end generates definitions:
  • Eq: eq_T : T -> T -> Bool.
  • Json (needs import json): T.toJson : T -> Json and T.fromJson : Json -> Either String T. The shape is {"k": constructor name, field name: value}, and the fields must be named (c (x : A)); an Option is null or the value, a pair is an array of two elements. A missing field, an extra field and an unknown constructor are errors with a path ($.items[0].body: missing field "c" of constructor sWhile). A data in a mutual block works too; a data with type parameters does not yet.

import json

data Shape = circle (r : Nat) | rect (w : Nat) (h : Nat) deriving Json

def text : Json.render (Shape.toJson (rect 2 3)) = "{\"k\":\"rect\",\"w\":2,\"h\":3}" := refl
def back : Json.decode Shape.fromJson "{\"k\":\"circle\",\"r\":1}" = right (circle 1) := refl

3.5 record

import std

record Point where { x : Nat; y : Nat }

def p : Point := { x := 1, y := 2 }
def px : Nat := p.x
def q : Point := { p with y := 5 }

• record name parameters… where { field : type; … }.
• Build with { field := value, … }; update with { r with field := value }; read a field with r.field.
• Each record is a type of its own: two records with fields of the same name are not confused.

3.6 class and instance (type classes)

import std

class Describe (A : Type) where { describe : A -> Nat }

instance describeBool : Describe Bool where { describe := fun b => match b with | true => 1 | false => 0 }

def describeTwice {A : Type} {{d : Describe A}} (a : A) : Nat := add (describe a) (describe a)

• class name parameters… [extends parents…] where { method : type; … }; a method can have a default, method : type := default.
• instance name parameters… : Class type where { method := implementation; … }, or instance name … : Class type := value.

3.7 namespace, section, open

import std

namespace Geo
def unit : Nat := 1
end Geo

def two : Nat := add Geo.unit Geo.unit

• namespace A … end A: the names defined inside get A. in front.
• open A: afterwards the names in A can be used directly (like C++’s using namespace A). A name can only be shortened when that is unambiguous: when the opened namespaces (or imported names) have two or more different f, the bare name f is an ambiguity error listing the candidates, so write the full name or use dot notation; your own definitions and local variables still shadow them.
• export open A: like open A, and files that import this module open A too (transitively along imports). export is syntax only right before open, and can still be a name.
• section … end: encloses a group of declarations (which can share parameters declared with variable).

3.8 Attributes and options

• @[simp], @[reducible], @[irreducible] and others are written before a declaration, one attribute per @[…].
• set_option maxHeartbeats N in before a declaration raises its checking budget.
• private: visible only in this module.

3.9 Notation declarations

• infixl 65 "+" := add, infixr, prefix, postfix: declare infix, prefix and postfix operators with their precedence (a larger number binds tighter).
• notation: notation in several parts. An operator can be used only after its declaration (or after importing the module that declares it).
• Operators are made of these characters: + ! # $ % & ~ \ ^ < > and mathematical symbols (⊕ ⊗ ≤ ≥ ≐ ≠ ≈ ∘ ⋅ and others). <-, ->, => and |> are built-in symbols, not operators; ==, <= and =? are operators of two characters.

3.10 Modalities

data B = tt | ff

modality secret : core -> core

def hide : secret.Type B := secret.mk tt

def keep (@secret b : B) : secret.Type B := secret.mk b

def apply (f : (@secret x : B) -> secret.Type B) (s : secret.Type B) : secret.Type B :=
  let secret.mk x := s in f x

• modality mu : m -> n: declares a modality (from mode m to mode n); mu.Type A is the modal type (in Unicode ⟨mu | A⟩).
• mu.mk a: puts a value under the modality, checking a under the lock mu: unannotated variables from outside cannot be used. let mu.mk x := s in ...: takes it apart, and x carries the annotation mu, usable only under the lock mu.
• (@mu x : A): a parameter with a modal annotation; (@mu x : A) -> B is a modal function type, whose argument is checked under the lock mu when it is applied. Function types with different modalities are different.
• law mu nu = rho: composition of locks (juxtaposition is composition, the outer one first; in Unicode mu ∘ nu); law mu => nu: a variable annotated mu can be used under the lock nu (nu can be id). The left side of a law has at least two modalities, and the laws must be confluent (overlapping laws must reduce to the same result both ways, checked when they are declared).
• Locks are checked by the elaborator and by the independent checker, separately. The rules are in chapter 10 of the typing rules.

3.11 codata (coinductive types)

data Nat = zero | succ Nat

codata Stream (A : Type) = head : A, tail : Stream A
codata Pair = head : Nat, other : Nat

def zeros : Stream Nat := { head => zero, tail => zeros }
def p : Pair := { head => succ zero, other => zero }

def a : Nat := head zeros
def b : Nat := head p
def c : Nat := Pair.head p
def d : Nat := zeros.tail.head

• codata name parameters… = projection : type, …: a type defined by what can be observed of it (and can be infinite); build a value with { projection => value, … }.
• Recursion must be inside { … } (guarded) and cannot be observed: { head => head s, … }, which reads itself back, is rejected.
• Projections live in the type’s namespace: Pair.head always means that type’s projection; s.head is looked up by the type of s. When two codata have projections of the same name, head x chooses by the type of x; an unapplied head (passed on as a function, say) means the last one declared, and when two imports both provide one, write the qualified name.

3.12 SProp (definitional proof irrelevance)

data N = zero | succ N
data STrue : SProp = sI
data SEmpty : SProp =
data SAnd (P Q : SProp) : SProp = sand P Q

def swap (P Q : SProp) (x : SAnd P Q) : SAnd Q P := match x with
  | sand p q => sand q p

def absurdS (A : Type) (e : SEmpty) : A := match e with

def irr (P : SProp) (F : P -> Type) (p q : P) (x : F p) : F q := x

• SProp (SProp 1, SProp l) is the sort of propositions: any two values of a type in SProp are definitionally equal (irr above holds without a proof).
• SProp l : Type (l+1); a function type whose codomain is in SProp is in SProp; a proposition quantifying over Type is in SProp 1 (predicative). SProp cannot be used as Type.
• data name … : SProp = …: declares a type in SProp. It can only be matched on to produce another proof (a type in SProp); a type without constructors is the exception, eliminating into any type. It cannot have path constructors.
• Path types and Glue are only in Type (proofs are equal anyway).
• SProp is a sort in expressions; to use it as a name, write r#SProp.

4. Expressions

4.1 Application and operators

• Function application is juxtaposition: f x y (first f x, then applied to y).
• Dot notation: e.f, where e’s type is T and T.f exists, is T.f e (with e as the first explicit parameter of T.f): c.get, (c.bump 2).get. A record’s fields still come first.
• The built-in operators, from loosest to tightest:
  • A -> B (function type, right-associative)
  • a = b (equality, import identity), a ≡ b (path; in ASCII Path a b), on the same level, not associative
  • A × B (product type, right-associative)
  • a - b, i /\ j, i \/ j (meet and join of the interval; ∧ and ∨ are aliases)
  • x |> f a (pipe: the same as f a x)
  • user-declared operators (for example a + b after import notation, and the boolean comparison a == b)
  • application (tightest)
• @f: explicit application, all implicit parameters must be given.

4.2 Types

• Type, Type 1: the types of types (universes). Type without a level is Type 0; to infer the level write Type _.
• (x : A) -> B x: a dependent function type; {x : A} -> B: a function type with an implicit parameter.
• (x : A) × B x: a dependent pair type.

4.3 fun

import std

def inc : Nat -> Nat := fun n => succ n
def add3 : Nat -> Nat -> Nat -> Nat := fun a b c => add a (add b c)
def swap : Pair Nat Nat -> Pair Nat Nat := fun (a, b) => mkPair b a

• fun x => e; a parameter can carry a type, fun (x : A) => e, or be implicit, fun {A} => e.
• fun (a, b) => e: takes a Pair (mkPair a b) apart directly; it can nest, fun (i, (c, r)) => ….

4.4 let

import std

def area (w : Nat) (h : Nat) : Nat :=
  let s := mul w h
  add s s

def inline : Nat := let x := 2 in mul x x

• let x := v in e; in can be left out: when let starts a line, the next line (in the same column as let) is the body.
• A type can be given: let x : Nat := v.

4.5 if

if condition then expression else expression. In an expression both branches must be written; the condition is a Bool.

4.6 match

import std

def describe (n : Nat) : Nat := match n with
  | zero => 0
  | succ zero => 1
  | succ (succ k) => match k with
    | zero => 2
    | succ j => 3

• match e with | pattern => expression | ….
• Indentation decides which match a branch belongs to: a more deeply indented | belongs to the inner match, so a nested match needs no parentheses.
• Patterns: a name (a binding), _, a constructor with subpatterns (succ (succ k)), a pair (a, b), a list [x, y], () (an impossible case, without =>), .x (a dot pattern decided by the type).
• Matching several expressions at once: match (a, b) with | (true, x) => … | (false, _) => …; each column splits by constructor, variables and _ catch the rest, and a combination nobody catches is reported as non-exhaustive (Lean’s match a, b with).
• When matching an expression (not just a variable), the expression is replaced by the constructor in each branch: the goal, and the hypotheses whose types depend on it, are refined. with (e) | … is another way to write the same thing (Agda’s with); nested withs belong to the inner or outer level by indentation.

data Nat = zero | succ Nat
data Bool = true | false

def isZero (n : Nat) : Bool := match n with
  | zero => true
  | succ k => false

def the (A : Type) (a : A) : A := a

def onlyZero (n : Nat) (h : isZero n ≡ true) : Nat := with (isZero n)
  | true => n
  | false => let wrong := the (false ≡ true) h in zero

4.7 Literals and the rest

• Tuples: (a, b); (a, b, c) is (a, (b, c)). When the expected type is Pair A B (or another type with one constructor and two fields), (a, b) is that constructor (mkPair a b); otherwise it is the dependent pair A × B, read with fst p and snd p. Both can be taken apart with the tuple pattern (a, b) (in fun, for and match).

import std
def scores : List (Pair Nat Nat) := [(1, 90), (2, 85)]
def total : Nat := scores |> map (fun (id, s) => s) |> foldr add 0
def t : total ≡ 175 := refl

• Lists: [1, 2, 3] (a trailing comma is allowed).
• Type ascription: (e : T).
• Holes: _ (for Cella to infer), ? or ?name (a hole left to fill; the check lists its type).

5. do: programs that run

import std
import io
import string

def countdown (n : Nat) : IO Unit := do
  let mut k := n
  for i in [1, 2, 3] do
    putStr f"step {i}"
    k := succ k
  if Nat.ble k 10 then
    putNat k
  else
    putStr "big"

def main : IO Unit := countdown 3

A do block has one statement per line, and indentation decides the block (a line in the same column is the next statement, a more deeply indented line continues the same statement). It can also be written on one line as do { statement; statement }.

Statement	Means
x <- e	run the action e and call its result x
_ <- e	run the action e and discard its result
let x := v	name a pure value
let mut x := v, x := v	a mutable variable and assignment
for x in xs do block	do it once for each element of the list; ys <- for … collects each result into a list
if c then block else block	else can be left out; else if chains
match e with | p => block	the branches are statement blocks
break, continue, return e	leave the loop, the next iteration, return early
e	run the action; the value of the last statement is the value of the whole do

Statements can also contain:

• (<- e): run the action e in the middle of an expression and take its result (run left to right): putNat (add (<- readNat) 1).
• e?: when e is an IO (Either E A), a failure makes the whole do return that failure.
• await t: wait for the task t to finish and take its result; tasks are made by async e or spawnTask job.

import std
import io

def main : IO Unit := do
  t <- async (pure 21)
  putNat (mul (await t) 2)

5.1 do in other monads

do is not only for IO: when the expected type is M A and M has a Monad instance, x <- e is bind e (fun x => …), and the last statement is the value of the block. let mut, for, break and return work the same way.

• Monad (import std): the methods pure : {A : Type} -> A -> M A and bind : {A : Type} -> {B : Type} -> M A -> (A -> M B) -> M B.
• Option, Either E and List have instances; IO’s instance is in io, and its pure and bind are the IO primitives IO.pure and IO.bind.
• When the expected type is IO, pure and bind are the IO primitives directly.
• When you write an instance for your own type, the methods can leave out the leading type parameters (pure := fun a => good a) or write them (pure := fun A a => good a).

import std

data Chk (A : Type) = good A | fail String

instance monadChk : Monad Chk where { pure := fun a => good a; bind := fun m f => match m with | good a => f a | fail w => fail w }

def both : Chk Nat := do
  a <- good 1
  b <- good 2
  pure (add a b)

When no instance is found, the error names the type: “no instance of Monad Box was found”.

5.2 Binding with a pattern: pattern <- e

The left side of <- can be a pattern: a type with one constructor (or a tuple) is taken apart directly; a pattern that can fail to match is written with | alternative, which runs when it does not match. When a pattern can fail and there is no alternative, the error names the missing constructor (failure is not hidden in the monad, as Haskell’s MonadFail does).

import std

data Two = two (a : Nat) (b : Nat)

def pairOf (n : Nat) : Option Two := some (two n (succ n))

def sum3 : Option Nat := do
  two a b <- pairOf 3
  pure (add a b)

def firstOr (xs : List Nat) : Option Nat := do
  cons x rest <- some xs | pure 0
  pure x

The rest of the block is what happens after a successful match. The brace form works too: do { two a b <- pairOf 3; pure (add a b) }.

6. Proofs

6.1 Paths and equality

• a = b is the type of proofs that a and b are equal (Eq _ a b; import std or import identity): only data and match, no cubical. refl proves a = a, and accepts what is equal after computation. The operations live under Eq, with the proof first, so dot notation works: h.sym, h.trans k, h.cong f, h.subst P x, Eq.transport h x; the constructor is Eq.refl (refl is chosen by the expected type).
• Path a b (in Unicode a ≡ b; built in, no import needed) is the type of paths from a to b (cubical equality, which univalence and higher inductive types rely on); refl proves Path a a too (written Path.refl; refl chooses Eq.refl or Path.refl by the expected type). Eq.toPath and Path.toEq (import identity.paths) convert between the two.
• Constructors belong to their type’s namespace: T.c is the constructor c of the type T (Nat.succ, Bool.true, Eq.refl); when nothing is confused, succ is written as it is.
• a == b is a boolean comparison (import notation): its result is a Bool, not a proof. The order relations of ordering.relations are written a <= b, a < b, and a =? b for the proposition that the two are equal; there is no infix multiplication (* is the product type: write mul a b).
• A path is a function on the interval: fun i => …, and p i is the point on the path.
• transport, transp, hcomp, Glue, ua and others are primitives of cubical type theory (ua turns an equivalence of types into a path).

import std
import identity

def addZeroId : add 2 0 = 2 := refl

def addZero : add 2 0 ≡ 2 := refl

def symm {A : Type} {a : A} {b : A} (p : a ≡ b) : b ≡ a := fun i => p (1 - i)

6.2 Tactics

Inside by { … }, tactics build a proof step by step; the steps are separated by line breaks or ;:

import std

theorem andComm (a : Bool) (b : Bool) : and a b ≡ and b a := by {
  cases a
  cases b
  rfl
  rfl
  cases b
  rfl
  rfl
}

Common tactics: intro, exact e, apply e, rfl, rewrite e, cases x, induction x, simp, ring, omega, linarith, decide, have x : T := e, constructor, left, right, exfalso, contradiction, try t, repeat t, first | t | t.

6.3 calc

calc a ≡ b by p; b ≡ c by q chains a series of equalities.

7. Layout rules in brief

• Top-level declarations start with a keyword; line breaks mean nothing special there.
• do blocks, the branch blocks of if, for and match inside a do, the branches of a match, and a let that starts a line decide their extent by indentation:
  • a line in the block’s column: the next statement (or branch);
  • a more deeply indented line: the same statement continues;
  • a less deeply indented line: the block ends.
• Layout is suspended inside the brackets ( ), [ ] and { }.

7.1 Formatting: cella fmt

• cella fmt files… formats in place; cella fmt --check files… changes nothing, lists what would change, and exits with a nonzero code if anything would.
• Only whitespace changes; the tokens (comments and syntactic sugar included) stay as written: several spaces on one line become one, at most one blank line in a row, and indentation is normalized to two spaces per level (equal indentation stays equal, deeper stays deeper).
• A line longer than 100 characters is broken at these places, in order: before a match branch’s |, after :=, before then and else, after =>, after ,, after ->, before a type’s :, and finally between the arguments of an application (one per line); inside brackets this recurses, each level indented two more. A line containing do, by, where or calc is not broken.
• The syntax tree parsed before and after formatting must be the same; where a definition would change, it is kept as it was, with a note.

Appendix: keywords

To use these words as names, write r#name (not needed after a dot). The browser’s keywords() gives the same list.

• Hard keywords (anywhere): Glue, Level, PathP, Size, Type, builtin, calc, class, codata, data, declare_syntax_cat, def, do, elab, else, end, extern, fst, fun, glue, hcomp, if, import, in, inductive, inf, infixl, infixr, instance, let, lmax, lsuc, lzero, macro_rules, match, mutual, namespace, notation, open, postfix, postulate, prefix, private, record, rule, section, set_option, snd, structure, syntax, tactic, then, theorem, transp, transport, ua, unglue, variable, where, with
• Contextual keywords (only in certain places): by, deriving, termination_by, decreasing_by, local, scoped, ensures
• Reserved (for modes and modalities): mode, modality, law, grades