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

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
- type Substitution = [Term]
- class Subst t where
  - substs :: Substitution -> t -> t
  - substUnder :: Nat -> Term -> t -> t
- idSub :: Telescope -> Substitution
- 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

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

Methods

apply :: t -> Args -> t

Instances

Apply Permutation |
Apply ClauseBody |
Apply Clause |
Apply Clauses |
Apply Sort |
Apply Type |
Apply Term |
Apply CompiledClauses |
Apply FunctionInverse |
Apply PrimFun |
Apply Defn |
Apply Definition |
Apply DisplayTerm |
Apply t => Apply [t] |
Apply t => Apply (Maybe t) |
Subst a => Apply (Tele a) |
Apply t => Apply (Blocked t) |
Apply a => Apply (Case a) |
(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

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

class Abstract t where

`(abstract args v) args --> v[args]`.

Methods

abstract :: Telescope -> t -> t

Instances

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

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

type Substitution = [Term]

Substitutions.

class Subst t where

Substitute a term for the nth free variable.

Methods

substs :: Substitution -> t -> t

substUnder :: Nat -> Term -> t -> t

Instances

Subst Pattern |
Subst ClauseBody |
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) |
Subst a => Subst (Abs a) |
Subst a => Subst (Tele a) |
Subst t => Subst (Blocked t) |
(Subst a, Subst b) => Subst (a, b) |

idSub :: Telescope -> Substitution

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

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

Instantiate an abstraction

class Raise t where

Add `k` to index of each open variable in `x`.

Methods

raiseFrom :: Nat -> Nat -> t -> t

Instances

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

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

data TelView

Constructors

TelV Telescope Type |

telView' :: Type -> TelView

telePi :: Telescope -> Type -> Type

telePi_ :: Telescope -> Type -> Type

Everything will be a pi.

dLub :: Sort -> Abs Sort -> Sort