|
|
|
|
|
|
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 | |
|
|
|
|
|
|
|
Pairs consisting of original and translated clauses.
| Constructors | Clauses | | maybeOriginalClause :: Maybe Clause | The original clause, before translation of record patterns.
Nothing if the translated clause is identical to the original
one.
| translatedClause :: Clause | The translated clause.
|
|
|
|
|
|
The original clause, before translation of record patterns.
|
|
|
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. (Note: This optimisation has been disabled.)
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. The body
binds the variables in the order they appear in the patterns.
For the purpose of the permutation and the body dot patterns count
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.1 |