Get the span of the source of this file.

Add an entry in the environment.

Parse a term. ```text term(prec) ::= operators(prec) { prefix "let" ::= let-expr prefix "if" ::= if-expr prefix "case

Get the size of the environment.

Add a definition to the context.

Evaluate a term using the evaluation environment

Returns the span of the current token in the source file.

Record a diagnostic.

Generate a fresh name based on the names that have already been used in the environment. We try to get close to the `name_hint`, adding a number if ne

Add a parameter the context, returning a variable that points to the introduced binder.

Ensures that the given term is a universe, returning the level of that universe and its elaborated form.

Return the level of the next variable to be added to the environment.

Evaluate a term using the evaluation environment.

Lookup an entry in the environment.

Skip by one character if the predicate matches the lookahead.

Consume the current token and load the next one. Return the old token.

Check that a given term conforms to an expected type. Returns the elaborated term.

Instantiate a closure in an environment of the given size.

Primitive entries.

Values to be used during evaluation.

Peek at the current lookahead token.

Convert the item into a pretty-printable document.

Add a bound variable the context, returning a variable that points to the correct binder.

Consume the current character and load the next one. Return the old token.

Apply a closure to an argument.

Get a slice to the contents of the file.

Evaluate a term in the environment that corresponds to the context in which the term was typed.

Bump the current position in the source string by one character, returning the current character or an unexpected end of file error.

Primitive entries.

Skip characters while the predicate matches the lookahead character.

Convert a variable level to a variable index in the current environment.

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

Synthesize the type of the term.

Ensures that the given term is a universe, returning the level of that universe.

Convert the context into a validation context.

Add a file to the database, returning the handle that can be used to refer to it again.

Add a fresh parameter the context, returning a variable that points to the introduced binder.

Apply a closure to an argument.

Insert metavariables based on the expected type.

Get a slice to the line start indices of the file.

Parse the trailing part of a function elimination. ```text fun-elim ::= arg ```

Skip some digits, separated by `_`, returning the number of digits consumed.

Synthesize the type of the given term. Metavariables are inserted based on the given `meta_insertion`. Returns the elaborated term and its synthesiz

Add a name-to-level substitution to the context.

Apply a closure to an argument.

Check that a given clause conforms to an expected type, and elaborates it into a case tree. Returns the elaborated term.

Check the given items and add them to the context.

Check the given items and add them to the context. Returns the elaborated items.

Check that a term conforms to a given type.

Concatenate a bunch of lines of documentation into a single string, removing comment prefixes if they are found.

Consume a decimal literal.

Consume an integer literal that uses a specific radix.

Get the handle that points to this file.

Lookup a the solution for a metavariable in the environment.

Parse the trailing part of a character literal.

Parse the trailing part of a floating point literal.

Parse the trailing part of a integer literal.

Parse zero-or-more function introduction parameters. ```text intro-params ::= intro-param ```

Parse an item. ```text item ::= DOC_COMMENT* IDENTIFIER ":" term(0) ";" | DOC_COMMENT* IDENTIFIER intro-param* (":" term(0))? "=" term(0) ";" ```

Parse a pattern. ```text pattern(prec) ::= operators(prec) { nilfix IDENTIFIER nilfix STRING_LITERAL nilfix CHAR_LITERAL nilfix INT_LITERAL nilfi

Parse the trailing part of a string literal.

Parse the trailing part of a variable.