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




class Apply t whereSource

Apply something to a bunch of arguments. Preserves blocking tags (application can never resolve blocking).


apply :: t -> Args -> tSource

piApply :: Type -> Args -> TypeSource

The type must contain the right number of pis without have to perform any reduction.

abstractArgs :: Abstract a => Args -> a -> aSource

type Substitution = [Term]Source


class Subst t whereSource

Substitute a term for the nth free variable.


substs :: Substitution -> t -> tSource

substUnder :: Nat -> Term -> t -> tSource

subst :: Subst t => Term -> t -> tSource

absApp :: Subst t => Abs t -> Term -> tSource

Instantiate an abstraction

class Raise t whereSource

Add k to index of each open variable in x.


raiseFrom :: Nat -> Nat -> t -> tSource


Raise Pattern 
Raise Sort 
Raise Type 
Raise Term 
Raise DisplayTerm 
Raise DisplayForm 
Raise AsBinding 
Raise t => Raise [t] 
Raise t => Raise (Maybe t) 
Raise t => Raise (Arg t) 
Raise t => Raise (Abs t) 
Raise a => Raise (Tele a) 
Raise t => Raise (Blocked t) 
(Raise a, Raise b) => Raise (a, b) 
Raise v => Raise (Map k v) 

raise :: Raise t => Nat -> t -> tSource

data TelView Source


TelV Telescope Type 

telePi_ :: Telescope -> Type -> TypeSource

Everything will be a pi.