The various universes involved in the uniqueness mechanism
A representation of Idris's old tactics that can be returned from custom
tactic implementations. Generate these using applyTactic.
Try the first tactic and resort to the second one on failure
Only run if the goal has the right type
Resolve function name, find matching arguments in the
context and compute the proof target
Apply both tactics in sequence
Introduce a new hole with a particular type
Move the current hole to the end
Intelligently construct the proof target from the context
Build a proof by applying contructors up to a maximum depth
Resolve an interface
Infer the proof target from the context
introduce all variables into the context
Introduce a named variable into the context, use the
first one if the given name is not found
Invoke the reflected rep. of another tactic
Turn a value into its reflected representation
Use a %reflection function
Turn a raw value back into a term
Use the given value to conclude the proof
Focus on a particular hole
Rewrite with an equality
Perform induction on a particular expression
Perform case analysis on a particular expression
Name a reflected term
Name a reflected term and type it
Normalise the goal
Do nothing
Fail with an error message
Attempt to fill the hole with source code information
A user-provided name
A name in some namespace.
The namespace is in reverse order, so (NS (UN "foo") ["B", "A"])
represents the name A.B.foo
Machine-chosen names
Special names, to make conflicts impossible and language features
predictable
Reflection of the well typed core language
A reference to some name (P for Parameter)
de Bruijn variables
Bind a variable
Apply one term to another
Embed a constant
Erased terms
The type of types along (with universe constraints)
Alternative universes for dealing with uniqueness
A source location in an Idris file
Either a source span or a source location. start and end
will be the same if it's a point location.
The file name of the source location
The line and column of the beginning of the source span
The line and column of the end of the source span
The file name of the source location
The line and column of the beginning of the source span
The line and column of the end of the source span
Raw terms without types
Things with a canonical representation as a reflected term.
This interface is intended to be used during proof automation and the
construction of custom tactics.
Types of named references
Either a source span or a source location. start and end
will be the same if it's a point location.
The file name of the source location
The line and column of the beginning of the source span
The line and column of the end of the source span
Error reports are a list of report parts
A human-readable string
An Idris name (to be semantically coloured)
An Idris term, to be pretty printed
A Raw term to be displayed by the compiler
An indented sub-report, to provide more details
Primitive constants
Types annotations for bound variables in different
binding contexts
the terms that can occur inside the binder, as type
annotations or bound values
Lambdas
the type of the argument
Function types.
The kind of arrow. Only relevant when dealing with
uniqueness, so you can usually pretend that this
field doesn't exist. For ordinary functions, use the
type of types here.
A let binder
the type of the bound variable
the bound value
A hole that can occur during elaboration, and must be filled
the type of the value that will eventually be put into the hole
A hole that will later become a top-level metavariable
A hole with a solution in it. Computationally inert.
the type of the value in the hole
the value in the hole
A pattern variable. These bindings surround the terms that make
up the left and right sides of pattern-matching definition
clauses.
the type of the pattern variable
The type of a pattern binding. This is to PVar as Pi is to
Lam.
the type of the pattern variable