|
|
|
|
|
|
Synopsis |
|
|
|
Documentation |
|
|
Raw values.
Def is used for both defined and undefined constants.
Assume there is a type declaration and a definition for
every constant, even if the definition is an empty
list of clauses.
| Constructors | |
|
|
|
|
|
|
Constructors | Type Term | | Prop | | Lub Sort Sort | | Suc Sort | | MetaS MetaId Args | | Inf | | DLub Sort (Abs Sort) | if the free variable occurs in the second sort
the whole thing should reduce to Inf, otherwise
it's the normal Lub
|
|
|
|
|
Something where a meta variable may block reduction.
| Constructors | |
|
|
|
Type of argument lists.
|
|
|
Sequence of types. An argument of the first type is bound in later types
and so on.
| Constructors | |
|
|
|
The body has (at least) one free variable.
| Constructors | |
|
|
|
|
|
|
|
A clause is a list of patterns and the clause body should Bind or
NoBind in the order the variables occur in the patterns. The NoBind
constructor is an optimisation to avoid substituting for variables that
aren't used.
The telescope contains the types of the pattern variables and the
permutation is how to get from the order the variables occur in the
patterns to the order they occur in the telescope. For the purpose of the
permutation dot patterns counts as variables.
TODO: change this!
| Constructors | |
|
|
|
|
|
|
Patterns are variables, constructors, or wildcards.
QName is used in ConP rather than Name since
a constructor might come from a particular namespace.
This also meshes well with the fact that values (i.e.
the arguments we are matching with) use QName.
| Constructors | |
|
|
|
|
|
|
Doesn't do any reduction.
|
|
|
Suggest a name for the first argument of a function of the given type.
|
|
Views
|
|
|
|
|
|
|
Smart constructors
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Get the next higher sort.
|
|
|
|
|
|
module Agda.Syntax.Abstract.Name |
|
Produced by Haddock version 2.6.0 |