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

Safe HaskellNone

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

composeS :: Substitution -> Substitution -> Substitution

applySubst (ρ composeS σ) v == applySubst ρ (applySubst σ v)

raise :: Subst t => Nat -> t -> t

raiseFrom :: Subst t => Nat -> Nat -> t -> t

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

substUnder :: Subst t => Nat -> Term -> t -> t

data TelV a

Constructors

TelV (Tele (Dom a)) a 

Instances

Functor TelV 
Typeable1 TelV 
(Eq a, Subst a) => Eq (TelV a) 
(Ord a, Subst a) => Ord (TelV a) 
Show a => Show (TelV a) 

mkPi :: Dom (String, Type) -> Type -> Type

mkPi dom t = telePi (telFromList [dom]) t

telePi_ :: Telescope -> Type -> Type

Everything will be a pi.

dLub :: Sort -> Abs Sort -> Sort

Dependent least upper bound, to assign a level to expressions like forall i -> Set i.

dLub s1 i.s2 = omega if i appears in the rigid variables of s2.

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

Instantiate an abstraction

absBody :: Subst t => Abs t -> t

mkAbs :: (Subst a, Free a) => String -> a -> Abs a

reAbs :: (Subst a, Free a) => Abs a -> Abs a

underAbs :: Subst a => (a -> b -> b) -> a -> Abs b -> Abs b

underAbs k a b applies k to a and the content of abstraction b and puts the abstraction back. a is raised if abstraction was proper such that at point of application of k and the content of b are at the same context. Precondition: a and b are at the same context at call time.

underLambdas :: Subst a => Int -> (a -> Term -> Term) -> a -> Term -> Term

underLambdas n k a b drops n initial Lams from b, performs operation k on a and the body of b, and puts the Lams back. a is raised correctly according to the number of abstractions.

sLub :: Sort -> Sort -> Sort