Parse the trailing part of a function introduction. ```text fun-ty ::= type-param+ "->" term(50 - 1) type-param ::= "(" IDENTIFIER+ ":" term(0) ")

Parse the trailing part of an if expression. ```text if-expr ::= term(0) "then" term(0) "else" term(0) ```

Parse a function introduction parameter. ```text intro-param ::= pattern(0) | "{" IDENTIFIER ("=" pattern(0))? "}" | "{{" IDENTIFIER ("=" pattern(0))

Parse the trailing part of a let expression. ```text let-expr ::= item+ "in" term(0) ```

Parse a module. ```text module ::= item ```

Parse the trailing part of a primitive. ```text primitive ::= STRING_LITERAL ```

Parse the trailing part of a record introduction. ```text record-intro ::= "{" (record-intro-field ";")* record-intro-field? "}" record-intro-

Parse the trailing part of a record type. ```text record-type ::= "{" (record-type-field ";")* record-type-field? "}" record-type-field ::=

Get the pretty width of the editor.

Read a value back into the core syntax, normalizing as required.

Read and evaluate the given file.

Run the CLI with the given options

Skip an ASCII character code.

Skip a unicode character code.

Synthesize the type of a literal.

Synthesize the type of the body of a clause, and elaborate it.

Convert a term to a pretty printable document.

Convert to a byte index, based on a unicode string and a starting index

Convert to a byte size, based on a unicode string

Returns the source of the current token.

Unify two values. If unification succeeds, the `value1` should be definitionally equal to, or a subtype of of `value2` in the updated metavariable env

Add a new entry to the environment.

Checks if a term is _alpha equivalent_ to another term. This means that the two terms share the same binding structure, while disregarding the actual

Construct an annotated term.

Check that this is a valid module. Returns the elaborated module.

Returns a string description of the literal kind.

The diagnostic that were emitted during lexing.

Create a new, empty context.

Create a new, empty context.