Agda-2.2.6: 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 

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 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) 
(Data a, 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 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.

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!

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.

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.