Agda-2.2.6: A dependently typed functional programming language and proof assistant Source code Contents Index

Agda.TypeChecking.Substitute

Synopsis

class Apply t where apply :: t -> Args -> t piApply :: Type -> Args -> Type class Abstract t where abstract :: Telescope -> t -> t abstractArgs :: Abstract a => Args -> a -> a class Subst t where substs :: [Term] -> t -> t substUnder :: Nat -> Term -> t -> t idSub :: Telescope -> [Term] subst :: Subst t => Term -> t -> t absApp :: Subst t => Abs t -> Term -> t class Raise t where raiseFrom :: Nat -> Nat -> t -> t raise :: Raise t => Nat -> t -> t data TelView = TelV Telescope Type telView :: Type -> TelView telePi :: Telescope -> Type -> Type telePi_ :: Telescope -> Type -> Type dLub :: Sort -> Abs Sort -> Sort

Documentation

class Apply t where Source

Apply something to a bunch of arguments. Preserves blocking tags (application can never resolve blocking). Methods apply :: t -> Args -> t Source

piApply :: Type -> Args -> Type Source

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

class Abstract t where Source

(abstract args v) args --> v[args]. Methods abstract :: Telescope -> t -> t Source

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

class Subst t where Source

Substitute a term for the nth free variable. Methods substs :: [Term] -> t -> t Source substUnder :: Nat -> Term -> t -> t Source

idSub :: Telescope -> [Term] Source

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

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

Instantiate an abstraction

class Raise t where Source

Add k to index of each open variable in x. Methods raiseFrom :: Nat -> Nat -> t -> t Source

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

data TelView Source

Constructors TelV Telescope Type

telView :: Type -> TelView Source

telePi :: Telescope -> Type -> Type Source

telePi_ :: Telescope -> Type -> Type Source

Everything will be a pi.

dLub :: Sort -> Abs Sort -> Sort Source

Produced by Haddock version 2.6.0