| 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

Instances

Apply Permutation
Apply ClauseBody
Apply Clause
Apply Telescope
Apply Sort
Apply Type
Apply Term
Apply FunctionInverse
Apply PrimFun
Apply Defn
Apply Definition
Apply DisplayTerm
Apply t => Apply ([] t)
Apply t => Apply (Maybe t)
Apply t => Apply (Blocked t)
(Apply a, Apply b) => Apply ((,) a b)
Apply v => Apply (Map k v)
(Apply a, Apply b, Apply c) => Apply ((,,) a b c)

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

Instances

Abstract Permutation
Abstract ClauseBody
Abstract Clause
Abstract Telescope
Abstract Sort
Abstract Type
Abstract Term
Abstract FunctionInverse
Abstract PrimFun
Abstract Defn
Abstract Definition
Abstract t => Abstract ([] t)
Abstract t => Abstract (Maybe t)
Abstract v => Abstract (Map k v)

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

Instances

Subst Pattern
Subst ClauseBody
Subst Telescope
Subst Sort
Subst Type
Subst Term
Subst DisplayTerm
Subst Equality
Subst AsBinding
Subst DotPatternInst
Subst a => Subst ([] a)
Subst a => Subst (Maybe a)
Subst a => Subst (Arg a)
(Data a, Subst a) => Subst (Abs a)
Subst t => Subst (Blocked t)
(Subst a, Subst b) => Subst ((,) a b)

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

Instances

Raise Telescope
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 t => Raise (Blocked t)
(Raise a, Raise b) => Raise ((,) a b)
Raise v => Raise (Map k v)

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.4.2