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

Consume float exponents, returning `true` if an exponent was found.

Returns a span in the source file.

Returns the string slice of the current token.

Convert a value to a pretty printable document.

Values to be used during evaluation.

Add a definition to the context.

Check the type of a literal in a context.

Check that this is a valid module.

Expect that `ty1` is a subtype of `ty2` in the current context.

Check whether a type is a subtype of another type.

Consume a number starting with zero.

Finish elaborating the patterns into a case tree.

Apply a function to an argument.

Case split on a literal.

Evaluate a primitive.

Return the field in from a record.

Evaluate a value further, if it's now possible due to updates made to the metavariable solutions.

Evaluate a value further, if it's now possible due to updates made to the metavariable solutions.

Create a fresh meta and return the meta applied to all of the currently bound vars.

Skip whitespace or line comment tokens.

Parse an argument term. ```text arg-term(prec) ::= operators(prec) { prefix "(" ::= parens prefix "Type" ::= universe

Parse the trailing part of a hole.

Parse the trailing part of a parenthesis grouping. ```text parens ::= term(0) ")" ```

Parse the trailing part of a record elimination. ```text record-elim ::= IDENTIFIER ```

Parse the trailing part of a universe. ```text universe ::= ("^" INT_LITERAL)? ```

Peek at the current lookahead character.

Convert the context into a pretty printing environment.

Shift the by the given amount, returning an error if maximum universe level has been reached.

Skip an escape.

Solve metavariables in the case where a metavariable has been found in a head position.

Return a slice of the source file, given a span.

Synthesize the type of the clauses, elaborating them into a case tree. Returns the elaborated term and its synthesized type.

Synthesize the type of the literal.

Expect that `ty1` is a subtype of `ty2` in the current context

Add a fresh definition to the context.

Add a solution to the given metavariable index.

Create a fresh metavariable index.

Check that the given case clauses conform to the expected type, and elaborate them into a case tree.

Check that the body of the given clause conforms to they expected type, and elaborate it.

Check that a literal conforms to a given type.

Check that a given parameter matches the expected application mode, and return the pattern inside it.

Scope check + occurs check a solution candidate.

Check that all entries in a spine are bound variables.

Consume a character literal.

Consume a identifier.

Consume a line comment.

Consume a doc comment.

Consume a number starting with a negative sign.

Consume a string literal.

Consume a symbol.

Consume a token, returning its tag or none on end of file.

Consume some whitespace.

Desugar punned fields.

Emit a token and reset the start position, ready for the next token.

Returns the span of the end of the file.

Evaluate an eliminator.

Interpret a primitive if there are enough function eliminators provided in the spine. `None` is returned if evaluation is stuck. Also known as [δ-red

Returns `true` if the item is a definition.

Lookup the de-bruijn index and the type annotation of a binder in the context using a user-defined name.

Lookup the type of a variable in the context.

Get the next expected parameter

Fully normalize a term by first evaluating it, then reading it back.

Parse the trailing part of a type annotation. ```text ann ::= term(20 - 1) ```

Parse an argument. ```text arg ::= arg-term(0) | "{" IDENTIFIER ("=" term(0))? "}" | "{{" IDENTIFIER ("=" term(0))? "}}" ```

Parse the trailing part of a case expression. ```text case-expr ::= arg-term(0) "{" (case-clause ";")* case-clause? "}" case-clause ::= pattern(0)

Parse the trailing part of a function arrow. ```text fun-arrow-type ::= term(50 - 1) ```

Parse the trailing part of a function introduction. ```text fun-intro ::= intro-param+ "=>" term(0) ```