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

Agda.TypeChecking.Substitute

Synopsis

Documentation

class Apply t where

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

Methods

apply :: t -> Args -> t

piApply :: Type -> Args -> Type

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

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

type Substitution = [Term]

Substitutions.

class Subst t where

Substitute a term for the nth free variable.

Methods

substs :: Substitution -> t -> t

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

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

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

Instantiate an abstraction

class Raise t where

Add k to index of each open variable in x.

Methods

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

Instances

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 -> t

data TelView

Constructors

TelV Telescope Type 

telePi_ :: Telescope -> Type -> Type

Everything will be a pi.

dLub :: Sort -> Abs Sort -> Sort