Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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 whereSource
Apply something to a bunch of arguments. Preserves blocking tags (application can never resolve blocking).
Methods
apply :: t -> Args -> tSource
show/hide Instances
piApply :: Type -> Args -> TypeSource
The type must contain the right number of pis without have to perform any reduction.
class Abstract t whereSource
(abstract args v) args --> v[args].
Methods
abstract :: Telescope -> t -> tSource
show/hide Instances
abstractArgs :: Abstract a => Args -> a -> aSource
class Subst t whereSource
Substitute a term for the nth free variable.
Methods
substs :: [Term] -> t -> tSource
substUnder :: Nat -> Term -> t -> tSource
show/hide Instances
idSub :: Telescope -> [Term]Source
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.
Methods
raiseFrom :: Nat -> Nat -> t -> tSource
show/hide Instances
raise :: Raise t => Nat -> t -> tSource
data TelView Source
Constructors
TelV Telescope Type
telView :: Type -> TelViewSource
telePi :: Telescope -> Type -> TypeSource
telePi_ :: Telescope -> Type -> TypeSource
Everything will be a pi.
dLub :: Sort -> Abs Sort -> SortSource
Produced by Haddock version 2.4.2