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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Substitute.Class

Contents

- Application
- Abstraction
- Substitution and raisingshiftingweakening
  - Identity instances
- Explicit substitutions
- Functions on abstractions

Synopsis

- class Apply t where
  - apply :: t -> Args -> t
  - applyE :: t -> Elims -> t
- applys :: Apply t => t -> [Term] -> t
- apply1 :: Apply t => t -> Term -> t
- class Abstract t where
  - abstract :: Telescope -> t -> t
- class DeBruijn t => Subst t a | a -> t where
  - applySubst :: Substitution' t -> a -> a
- raise :: Subst t a => Nat -> a -> a
- raiseFrom :: Subst t a => Nat -> Nat -> a -> a
- subst :: Subst t a => Int -> t -> a -> a
- strengthen :: Subst t a => Empty -> a -> a
- substUnder :: Subst t a => Nat -> t -> a -> a
- idS :: Substitution' a
- wkS :: Int -> Substitution' a -> Substitution' a
- raiseS :: Int -> Substitution' a
- consS :: DeBruijn a => a -> Substitution' a -> Substitution' a
- singletonS :: DeBruijn a => Int -> a -> Substitution' a
- inplaceS :: Subst a a => Int -> a -> Substitution' a
- liftS :: Int -> Substitution' a -> Substitution' a
- dropS :: Int -> Substitution' a -> Substitution' a
- composeS :: Subst a a => Substitution' a -> Substitution' a -> Substitution' a
- splitS :: Int -> Substitution' a -> (Substitution' a, Substitution' a)
- (++#) :: DeBruijn a => [a] -> Substitution' a -> Substitution' a
- prependS :: DeBruijn a => Empty -> [Maybe a] -> Substitution' a -> Substitution' a
- parallelS :: DeBruijn a => [a] -> Substitution' a
- compactS :: DeBruijn a => Empty -> [Maybe a] -> Substitution' a
- strengthenS :: Empty -> Int -> Substitution' a
- lookupS :: Subst a a => Substitution' a -> Nat -> a
- absApp :: Subst t a => Abs a -> t -> a
- lazyAbsApp :: Subst t a => Abs a -> t -> a
- noabsApp :: Subst t a => Empty -> Abs a -> a
- absBody :: Subst t a => Abs a -> a
- mkAbs :: (Subst t a, Free a) => ArgName -> a -> Abs a
- reAbs :: (Subst t a, Free a) => Abs a -> Abs a
- underAbs :: Subst t a => (a -> b -> b) -> a -> Abs b -> Abs b
- underLambdas :: Subst Term a => Int -> (a -> Term -> Term) -> a -> Term -> Term

# Application

class Apply t where Source #

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

Minimal complete definition

applyE

Methods

apply :: t -> Args -> t Source #

applyE :: t -> Elims -> t Source #

Instances

Apply Permutation Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Permutation -> Args -> Permutation Source # applyE :: Permutation -> Elims -> Permutation Source #
Apply Clause Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Clause -> Args -> Clause Source # applyE :: Clause -> Elims -> Clause Source #
Apply Sort Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Sort -> Args -> Sort Source # applyE :: Sort -> Elims -> Sort Source #
Apply Term Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Term -> Args -> Term Source # applyE :: Term -> Elims -> Term Source #
Apply CompiledClauses Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: CompiledClauses -> Args -> CompiledClauses Source # applyE :: CompiledClauses -> Elims -> CompiledClauses Source #
Apply FunctionInverse Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: FunctionInverse -> Args -> FunctionInverse Source # applyE :: FunctionInverse -> Elims -> FunctionInverse Source #
Apply PrimFun Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: PrimFun -> Args -> PrimFun Source # applyE :: PrimFun -> Elims -> PrimFun Source #
Apply Defn Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Defn -> Args -> Defn Source # applyE :: Defn -> Elims -> Defn Source #
Apply ProjLams Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: ProjLams -> Args -> ProjLams Source # applyE :: ProjLams -> Elims -> ProjLams Source #
Apply Projection Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Projection -> Args -> Projection Source # applyE :: Projection -> Elims -> Projection Source #
Apply ExtLamInfo Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: ExtLamInfo -> Args -> ExtLamInfo Source # applyE :: ExtLamInfo -> Elims -> ExtLamInfo Source #
Apply System Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: System -> Args -> System Source # applyE :: System -> Elims -> System Source #
Apply NumGeneralizableArgs Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: NumGeneralizableArgs -> Args -> NumGeneralizableArgs Source # applyE :: NumGeneralizableArgs -> Elims -> NumGeneralizableArgs Source #
Apply Definition Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Definition -> Args -> Definition Source # applyE :: Definition -> Elims -> Definition Source #
Apply RewriteRule Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: RewriteRule -> Args -> RewriteRule Source # applyE :: RewriteRule -> Elims -> RewriteRule Source #
Apply DisplayTerm Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: DisplayTerm -> Args -> DisplayTerm Source # applyE :: DisplayTerm -> Elims -> DisplayTerm Source #
Apply t => Apply [t] Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: [t] -> Args -> [t] Source # applyE :: [t] -> Elims -> [t] Source #
Apply [NamedArg (Pattern' a)] Source # | Make sure we only drop variable patterns.
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: [NamedArg (Pattern' a)] -> Args -> [NamedArg (Pattern' a)] Source # applyE :: [NamedArg (Pattern' a)] -> Elims -> [NamedArg (Pattern' a)] Source #
Apply [Occurrence] Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: [Occurrence] -> Args -> [Occurrence] Source # applyE :: [Occurrence] -> Elims -> [Occurrence] Source #
Apply [Polarity] Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: [Polarity] -> Args -> [Polarity] Source # applyE :: [Polarity] -> Elims -> [Polarity] Source #
Apply t => Apply (Maybe t) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Maybe t -> Args -> Maybe t Source # applyE :: Maybe t -> Elims -> Maybe t Source #
DoDrop a => Apply (Drop a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Drop a -> Args -> Drop a Source # applyE :: Drop a -> Elims -> Drop a Source #
Apply t => Apply (Blocked t) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Blocked t -> Args -> Blocked t Source # applyE :: Blocked t -> Elims -> Blocked t Source #
Subst Term a => Apply (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Tele a -> Args -> Tele a Source # applyE :: Tele a -> Elims -> Tele a Source #
Apply a => Apply (Case a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Case a -> Args -> Case a Source # applyE :: Case a -> Elims -> Case a Source #
Apply a => Apply (WithArity a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: WithArity a -> Args -> WithArity a Source # applyE :: WithArity a -> Elims -> WithArity a Source #
(Apply a, Apply b) => Apply (a, b) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: (a, b) -> Args -> (a, b) Source # applyE :: (a, b) -> Elims -> (a, b) Source #
Apply v => Apply (HashMap k v) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: HashMap k v -> Args -> HashMap k v Source # applyE :: HashMap k v -> Elims -> HashMap k v Source #
Apply v => Apply (Map k v) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Map k v -> Args -> Map k v Source # applyE :: Map k v -> Elims -> Map k v Source #
(Apply a, Apply b, Apply c) => Apply (a, b, c) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: (a, b, c) -> Args -> (a, b, c) Source # applyE :: (a, b, c) -> Elims -> (a, b, c) Source #

applys :: Apply t => t -> [Term] -> t Source #

Apply to some default arguments.

apply1 :: Apply t => t -> Term -> t Source #

Apply to a single default argument.

# Abstraction

class Abstract t where Source #

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

Methods

abstract :: Telescope -> t -> t Source #

Instances

Abstract Permutation Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Permutation -> Permutation Source #
Abstract Clause Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Clause -> Clause Source #
Abstract Sort Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Sort -> Sort Source #
Abstract Telescope Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Telescope -> Telescope Source #
Abstract Type Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Type -> Type Source #
Abstract Term Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Term -> Term Source #
Abstract CompiledClauses Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> CompiledClauses -> CompiledClauses Source #
Abstract FunctionInverse Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> FunctionInverse -> FunctionInverse Source #
Abstract PrimFun Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> PrimFun -> PrimFun Source #
Abstract Defn Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Defn -> Defn Source #
Abstract ProjLams Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> ProjLams -> ProjLams Source #
Abstract Projection Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Projection -> Projection Source #
Abstract System Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> System -> System Source #
Abstract NumGeneralizableArgs Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> NumGeneralizableArgs -> NumGeneralizableArgs Source #
Abstract Definition Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Definition -> Definition Source #
Abstract RewriteRule Source # | `tel ⊢ (Γ ⊢ lhs ↦ rhs : t)` becomes `tel, Γ ⊢ lhs ↦ rhs : t)` we do not need to change lhs, rhs, and t since they live in Γ. See 'Abstract Clause'.
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> RewriteRule -> RewriteRule Source #
Abstract t => Abstract [t] Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> [t] -> [t] Source #
Abstract [Occurrence] Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> [Occurrence] -> [Occurrence] Source #
Abstract [Polarity] Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> [Polarity] -> [Polarity] Source #
Abstract t => Abstract (Maybe t) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Maybe t -> Maybe t Source #
DoDrop a => Abstract (Drop a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Drop a -> Drop a Source #
Abstract a => Abstract (Case a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Case a -> Case a Source #
Abstract a => Abstract (WithArity a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> WithArity a -> WithArity a Source #
Abstract v => Abstract (HashMap k v) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> HashMap k v -> HashMap k v Source #
Abstract v => Abstract (Map k v) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Map k v -> Map k v Source #

# Substitution and raisingshiftingweakening

class DeBruijn t => Subst t a | a -> t where Source #

Apply a substitution.

Methods

applySubst :: Substitution' t -> a -> a Source #

Instances

Subst TTerm TAlt Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods applySubst :: Substitution' TTerm -> TAlt -> TAlt Source #
Subst TTerm TTerm Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods applySubst :: Substitution' TTerm -> TTerm -> TTerm Source #
Subst DeBruijnPattern DeBruijnPattern Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' DeBruijnPattern -> DeBruijnPattern -> DeBruijnPattern Source #
Subst Term () Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> () -> () Source #
Subst Term String Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> String -> String Source #
Subst Term Range Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Range -> Range Source #
Subst Term QName Source # |
Instance details Defined in Agda.TypeChecking.Substitute.Class Methods applySubst :: Substitution' Term -> QName -> QName Source #
Subst Term Name Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Name -> Name Source #
Subst Term EqualityView Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> EqualityView -> EqualityView Source #
Subst Term ConPatternInfo Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> ConPatternInfo -> ConPatternInfo Source #
Subst Term Pattern Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Pattern -> Pattern Source #
Subst Term LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> LevelAtom -> LevelAtom Source #
Subst Term PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> PlusLevel -> PlusLevel Source #
Subst Term Level Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Level -> Level Source #
Subst Term Sort Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Sort -> Sort Source #
Subst Term Term Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Term -> Term Source #
Subst Term ProblemEq Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> ProblemEq -> ProblemEq Source #
Subst Term Candidate Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Candidate -> Candidate Source #
Subst Term DisplayTerm Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> DisplayTerm -> DisplayTerm Source #
Subst Term DisplayForm Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> DisplayForm -> DisplayForm Source #
Subst Term Constraint Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Constraint -> Constraint Source #
Subst Term AbsurdPattern Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods applySubst :: Substitution' Term -> AbsurdPattern -> AbsurdPattern Source #
Subst Term DotPattern Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods applySubst :: Substitution' Term -> DotPattern -> DotPattern Source #
Subst Term AsBinding Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods applySubst :: Substitution' Term -> AsBinding -> AsBinding Source #
Subst Term SizeConstraint Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods applySubst :: Substitution' Term -> SizeConstraint -> SizeConstraint Source #
Subst Term SizeMeta Source # |
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods applySubst :: Substitution' Term -> SizeMeta -> SizeMeta Source #
Subst Term CType Source # |
Instance details Defined in Agda.TypeChecking.Rules.Data Methods applySubst :: Substitution' Term -> CType -> CType Source #
Subst Term LType Source # |
Instance details Defined in Agda.TypeChecking.Rules.Data Methods applySubst :: Substitution' Term -> LType -> LType Source #
Subst NLPat RewriteRule Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' NLPat -> RewriteRule -> RewriteRule Source #
Subst NLPat NLPType Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' NLPat -> NLPType -> NLPType Source #
Subst NLPat NLPat Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' NLPat -> NLPat -> NLPat Source #
Subst SplitPattern SplitPattern Source # |
Instance details Defined in Agda.TypeChecking.Coverage.Match Methods applySubst :: Substitution' SplitPattern -> SplitPattern -> SplitPattern Source #
Subst t a => Subst t [a] Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> [a] -> [a] Source #
Subst t a => Subst t (Maybe a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> Maybe a -> Maybe a Source #
Subst t a => Subst t (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> Dom a -> Dom a Source #
Subst t a => Subst t (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> Arg a -> Arg a Source #
Subst t a => Subst t (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> Abs a -> Abs a Source #
Subst t a => Subst t (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> Elim' a -> Elim' a Source #
Subst t a => Subst t (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> Tele a -> Tele a Source #
Subst t a => Subst t (Blocked a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> Blocked a -> Blocked a Source #
Subst a a => Subst a (Substitution' a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' a -> Substitution' a -> Substitution' a Source #
Subst Term a => Subst Term (Type' a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' Term -> Type' a -> Type' a Source #
Subst Term (Problem a) Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods applySubst :: Substitution' Term -> Problem a -> Problem a Source #
(Subst t a, Subst t b) => Subst t (a, b) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> (a, b) -> (a, b) Source #
(Ord k, Subst t a) => Subst t (Map k a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> Map k a -> Map k a Source #
Subst t a => Subst t (Named name a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> Named name a -> Named name a Source #
Subst Term (SizeExpr' NamedRigid SizeMeta) Source # | Only for `raise`.
Instance details Defined in Agda.TypeChecking.SizedTypes.Solve Methods applySubst :: Substitution' Term -> SizeExpr' NamedRigid SizeMeta -> SizeExpr' NamedRigid SizeMeta Source #
(Subst t a, Subst t b, Subst t c) => Subst t (a, b, c) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> (a, b, c) -> (a, b, c) Source #
(Subst t a, Subst t b, Subst t c, Subst t d) => Subst t (a, b, c, d) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' t -> (a, b, c, d) -> (a, b, c, d) Source #

raise :: Subst t a => Nat -> a -> a Source #

raiseFrom :: Subst t a => Nat -> Nat -> a -> a Source #

subst :: Subst t a => Int -> t -> a -> a Source #

Replace de Bruijn index i by a `Term` in something.

strengthen :: Subst t a => Empty -> a -> a Source #

substUnder :: Subst t a => Nat -> t -> a -> a Source #

Replace what is now de Bruijn index 0, but go under n binders. `substUnder n u == subst n (raise n u)`.

## Identity instances

# Explicit substitutions

idS :: Substitution' a Source #

wkS :: Int -> Substitution' a -> Substitution' a Source #

raiseS :: Int -> Substitution' a Source #

consS :: DeBruijn a => a -> Substitution' a -> Substitution' a Source #

singletonS :: DeBruijn a => Int -> a -> Substitution' a Source #

To replace index `n` by term `u`, do `applySubst (singletonS n u)`. `Γ, Δ ⊢ u : A --------------------------------- Γ, Δ ⊢ singletonS |Δ| u : Γ, A, Δ`

inplaceS :: Subst a a => Int -> a -> Substitution' a Source #

Single substitution without disturbing any deBruijn indices. `Γ, A, Δ ⊢ u : A --------------------------------- Γ, A, Δ ⊢ inplace |Δ| u : Γ, A, Δ`

liftS :: Int -> Substitution' a -> Substitution' a Source #

Lift a substitution under k binders.

dropS :: Int -> Substitution' a -> Substitution' a Source #

            Γ ⊢ ρ : Δ, Ψ
         -------------------
         Γ ⊢ dropS |Ψ| ρ : Δ

composeS :: Subst a a => Substitution' a -> Substitution' a -> Substitution' a Source #

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

splitS :: Int -> Substitution' a -> (Substitution' a, Substitution' a) Source #

(++#) :: DeBruijn a => [a] -> Substitution' a -> Substitution' a infixr 4 Source #

prependS :: DeBruijn a => Empty -> [Maybe a] -> Substitution' a -> Substitution' a Source #

         Γ ⊢ ρ : Δ  Γ ⊢ reverse vs : Θ
         ----------------------------- (treating Nothing as having any type)
           Γ ⊢ prependS vs ρ : Δ, Θ

parallelS :: DeBruijn a => [a] -> Substitution' a Source #

compactS :: DeBruijn a => Empty -> [Maybe a] -> Substitution' a Source #

strengthenS :: Empty -> Int -> Substitution' a Source #

Γ ⊢ (strengthenS ⊥ |Δ|) : Γ,Δ

lookupS :: Subst a a => Substitution' a -> Nat -> a Source #

# Functions on abstractions

absApp :: Subst t a => Abs a -> t -> a Source #

Instantiate an abstraction. Strict in the term.

lazyAbsApp :: Subst t a => Abs a -> t -> a Source #

Instantiate an abstraction. Lazy in the term, which allow it to be (throwImpossible (Impossible "srcfullAgdaTypeCheckingSubstitute/Class.hs" 236)) in the case where the variable shouldn't be used but we cannot use `noabsApp`. Used in Apply.

noabsApp :: Subst t a => Empty -> Abs a -> a Source #

Instantiate an abstraction that doesn't use its argument.

absBody :: Subst t a => Abs a -> a Source #

mkAbs :: (Subst t a, Free a) => ArgName -> a -> Abs a Source #

reAbs :: (Subst t a, Free a) => Abs a -> Abs a Source #

underAbs :: Subst t a => (a -> b -> b) -> a -> Abs b -> Abs b Source #

`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 Term a => Int -> (a -> Term -> Term) -> a -> Term -> Term Source #

`underLambdas n k a b` drops `n` initial `Lam`s from `b`, performs operation `k` on `a` and the body of `b`, and puts the `Lam`s back. `a` is raised correctly according to the number of abstractions.