Agda-2.2.10: A dependently typed functional programming language and proof assistant





data Term Source

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.


Var Nat Args 
Lam Hiding (Abs Term)

terms are beta normal

Lit Literal 
Def QName Args 
Con QName Args 
Pi (Arg Type) (Abs Type) 
Fun (Arg Type) Type 
Sort Sort 
MetaV MetaId Args 

nuked irrelevant and other stuff

data Sort Source


Type Term 
Lub Sort Sort 
Suc Sort 
MetaS MetaId Args 
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

data Blocked t Source

Something where a meta variable may block reduction.


Blocked MetaId t 
NotBlocked t 

type Args = [Arg Term]Source

Type of argument lists.

data Tele a Source

Sequence of types. An argument of the first type is bound in later types and so on.


ExtendTel a (Abs (Tele a)) 


Functor Tele 
Typeable1 Tele 
Eq a => Eq (Tele a) 
Data a => Data (Tele a) 
Ord a => Ord (Tele a) 
Show a => Show (Tele a) 
Sized (Tele a) 
KillRange a => KillRange (Tele a) 
Free a => Free (Tele a) 
Raise a => Raise (Tele a) 
Subst a => Subst (Tele a) 
Subst a => Apply (Tele a) 
InstantiateFull a => InstantiateFull (Tele a) 
Normalise a => Normalise (Tele a) 
ComputeOccurrences a => ComputeOccurrences (Tele a) 

data Abs a Source

The body has (at least) one free variable.




absName :: String
absBody :: a


Functor Abs 
Typeable1 Abs 
Foldable Abs 
Traversable Abs 
Eq a => Eq (Abs a) 
Data a => Data (Abs a) 
Ord a => Ord (Abs a) 
Show a => Show (Abs a) 
Sized a => Sized (Abs a) 
KillRange a => KillRange (Abs a) 
Free a => Free (Abs a) 
TermLike a => TermLike (Abs a) 
Strict a => Strict (Abs a) 
Raise t => Raise (Abs t) 
Subst a => Subst (Abs a) 
(Subst a, AbstractTerm a) => AbstractTerm (Abs a) 
KillVar a => KillVar (Abs a) 
GenC a => GenC (Abs a) 
EmbPrj a => EmbPrj (Abs a) 
InstantiateFull t => InstantiateFull (Abs t) 
Normalise t => Normalise (Abs t) 
Reduce t => Reduce (Abs t) 
Instantiate t => Instantiate (Abs t) 
Occurs a => Occurs (Abs a) 
ComputeOccurrences a => ComputeOccurrences (Abs a) 
HasPolarity a => HasPolarity (Abs a) 
ShrinkC a b => ShrinkC (Abs a) (Abs b) 
Reify i a => Reify (Abs i) (Name, a) 

data Clauses Source

Pairs consisting of original and translated 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.

originalClause :: Clauses -> ClauseSource

The original clause, before translation of record patterns.

data Clause Source

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!

data Pattern Source

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.


VarP String 
DotP Term 
ConP QName (Maybe (Arg Type)) [Arg Pattern]

The type is Just t' iff the pattern is a record pattern. The scope used for the type is given by any outer scope plus the clause's telescope (clauseTel).

LitP Literal 

arity :: Type -> NatSource

Doesn't do any reduction.

argName :: Type -> StringSource

Suggest a name for the first argument of a function of the given type.


data FunView Source


FunV (Arg Type) Term

second arg is the entire type (Pi or Fun).

NoFunV Term 

Smart constructors

sSuc :: Sort -> SortSource

Get the next higher sort.