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

Safe HaskellNone

Agda.TypeChecking.Substitute

Synopsis

Documentation

class Apply t whereSource

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

Methods

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

composeS :: Substitution -> Substitution -> SubstitutionSource

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

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

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

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

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

data TelV a Source

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

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

telePi_ :: Telescope -> Type -> TypeSource

Everything will be a pi.

dLub :: Sort -> Abs Sort -> SortSource

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

Instantiate an abstraction

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

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

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

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

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

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.