Agda-2.6.4.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Substitute.Class

Synopsis

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

Instances details
Apply BraveTerm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply Clause Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

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

Apply Definition Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply Defn Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Defn -> Args -> Defn Source #

applyE :: Defn -> Elims -> Defn Source #

Apply DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply ExtLamInfo Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply FunctionInverse Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply PrimFun Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply Projection Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply System Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply Permutation Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

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 #

TermSubst 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

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 (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 #

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 #

Apply [NamedArg (Pattern' a)] Source #

Make sure we only drop variable patterns.

Instance details

Defined in Agda.TypeChecking.Substitute

Apply [Polarity] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply [Occurrence] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Apply t => Apply [t] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

applyE :: [t] -> Elims -> [t] 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 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 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 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

Instances details
Abstract Clause Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Sort Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Term Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Type Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract CompiledClauses Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Definition Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Defn Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract FunctionInverse Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract NumGeneralizableArgs Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract PrimFun Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract ProjLams Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Projection Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

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

Abstract System Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract Permutation Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

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

DoDrop a => Abstract (Drop a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> Drop a -> Drop a Source #

Abstract t => Abstract (Maybe t) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

Abstract [Polarity] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract [Occurrence] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Abstract t => Abstract [t] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> [t] -> [t] 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 #

Abstract v => Abstract (HashMap k v) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

abstract :: Telescope -> HashMap k v -> HashMap k v Source #

Substitution and shifting/weakening/strengthening

class DeBruijn (SubstArg a) => Subst a where Source #

Apply a substitution.

Minimal complete definition

Nothing

Associated Types

type SubstArg a Source #

Methods

applySubst :: Substitution' (SubstArg a) -> a -> a Source #

default applySubst :: forall (f :: Type -> Type) b. (a ~ f b, Functor f, Subst b, SubstArg a ~ SubstArg b) => Substitution' (SubstArg a) -> a -> a Source #

Instances

Instances details
Subst ProblemEq Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg ProblemEq 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Name Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Name 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst QName Source # 
Instance details

Defined in Agda.TypeChecking.Substitute.Class

Associated Types

type SubstArg QName 
Instance details

Defined in Agda.TypeChecking.Substitute.Class

Subst BraveTerm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg BraveTerm 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst ConPatternInfo Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg ConPatternInfo 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst DeBruijnPattern Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg DeBruijnPattern 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst EqualityTypeData Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg EqualityTypeData 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg EqualityView 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Pattern Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Pattern 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Term 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Range Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Range 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst TAlt Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Associated Types

type SubstArg TAlt 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Subst TTerm Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Associated Types

type SubstArg TTerm 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Subst SplitPattern Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.Match

Associated Types

type SubstArg SplitPattern 
Instance details

Defined in Agda.TypeChecking.Coverage.Match

Subst Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Candidate 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst CompareAs Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg CompareAs 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg Constraint 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg DisplayForm 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg DisplayTerm 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst LetBinding Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg LetBinding 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst NLPSort Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg NLPSort 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg NLPType 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg NLPat 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst RewriteRule Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg RewriteRule 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst CType Source # 
Instance details

Defined in Agda.TypeChecking.Primitive.Cubical

Associated Types

type SubstArg CType 
Instance details

Defined in Agda.TypeChecking.Primitive.Cubical

Subst LType Source # 
Instance details

Defined in Agda.TypeChecking.Primitive.Cubical

Associated Types

type SubstArg LType 
Instance details

Defined in Agda.TypeChecking.Primitive.Cubical

Subst AbsurdPattern Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Associated Types

type SubstArg AbsurdPattern 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Subst AsBinding Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Associated Types

type SubstArg AsBinding 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Subst DotPattern Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Associated Types

type SubstArg DotPattern 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Subst SizeConstraint Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Associated Types

type SubstArg SizeConstraint 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Subst SizeMeta Source # 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Associated Types

type SubstArg SizeMeta 
Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

Subst () Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg () 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg () = Term

Methods

applySubst :: Substitution' (SubstArg ()) -> () -> () Source #

Subst a => Subst (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Arg a) 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg (Arg a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Arg a)) -> Arg a -> Arg a Source #

Subst a => Subst (WithHiding a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (WithHiding a) 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst a => Subst (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Abs a) 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg (Abs a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Abs a)) -> Abs a -> Abs a Source #

Subst a => Subst (Blocked a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Blocked a) 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst a => Subst (Level' a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Level' a) 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg (Level' a) = SubstArg a
Subst a => Subst (PlusLevel' a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (PlusLevel' a) 
Instance details

Defined in Agda.TypeChecking.Substitute

(Coercible a Term, Subst a) => Subst (Sort' a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Sort' a) 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg (Sort' a) = SubstArg a
EndoSubst a => Subst (Substitution' a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Substitution' a) 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg (Substitution' a) = a
Subst a => Subst (Tele a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Tele a) 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg (Tele a) = SubstArg a
Subst a => Subst (Elim' a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Elim' a) 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg (Elim' a) = SubstArg a
Subst t => Subst (SingleLevel' t) Source # 
Instance details

Defined in Agda.TypeChecking.Level

Associated Types

type SubstArg (SingleLevel' t) 
Instance details

Defined in Agda.TypeChecking.Level

Subst a => Subst (AbsN a) Source # 
Instance details

Defined in Agda.TypeChecking.Names

Associated Types

type SubstArg (AbsN a) 
Instance details

Defined in Agda.TypeChecking.Names

type SubstArg (AbsN a) = SubstArg a
Subst (Problem a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Associated Types

type SubstArg (Problem a) 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

type SubstArg (Problem a) = Term
Subst a => Subst (Maybe a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Maybe a) 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg (Maybe a) = SubstArg a
Subst a => Subst [a] Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg [a] 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg [a] = SubstArg a

Methods

applySubst :: Substitution' (SubstArg [a]) -> [a] -> [a] Source #

Subst a => Subst (Named name a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Named name a) 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg (Named name a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Named name a)) -> Named name a -> Named name a Source #

(Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (Dom' a b) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Dom' a b) 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg (Dom' a b) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Dom' a b)) -> Dom' a b -> Dom' a b Source #

(Coercible a Term, Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (Type'' a b) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Type'' a b) 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg (Type'' a b) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Type'' a b)) -> Type'' a b -> Type'' a b Source #

Subst (SizeExpr' NamedRigid SizeMeta) Source #

Only for raise.

Instance details

Defined in Agda.TypeChecking.SizedTypes.Solve

(Ord k, Subst a) => Subst (Map k a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Map k a) 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg (Map k a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Map k a)) -> Map k a -> Map k a Source #

(Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (a, b) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (a, b) 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg (a, b) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (a, b)) -> (a, b) -> (a, b) Source #

(Subst a, Subst b, Subst c, SubstArg a ~ SubstArg b, SubstArg b ~ SubstArg c) => Subst (a, b, c) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (a, b, c) 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg (a, b, c) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (a, b, c)) -> (a, b, c) -> (a, b, c) Source #

(Subst a, Subst b, Subst c, Subst d, SubstArg a ~ SubstArg b, SubstArg b ~ SubstArg c, SubstArg c ~ SubstArg d) => Subst (a, b, c, d) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (a, b, c, d) 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg (a, b, c, d) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (a, b, c, d)) -> (a, b, c, d) -> (a, b, c, d) Source #

type SubstWith t a = (Subst a, SubstArg a ~ t) Source #

Simple constraint alias for a Subst instance a with arg type t.

type EndoSubst a = SubstWith a a Source #

Subst instance whose agument type is itself

type TermSubst a = SubstWith Term a Source #

Subst instance whose argument type is Term

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

Raise de Bruijn index, i.e. weakening

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

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

Replace de Bruijn index i by a Term in something.

strengthen :: Subst a => Impossible -> a -> a Source #

substUnder :: Subst a => Nat -> SubstArg a -> 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

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 :: EndoSubst 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 :: EndoSubst a => Substitution' a -> Substitution' a -> Substitution' a Source #

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

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

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

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

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

       Γ ⊢ reverse vs : Δ
     -----------------------------
       Γ ⊢ parallelS vs ρ : Γ, Δ
  

Note the Γ in Γ, Δ.

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

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

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

A "smart" variant of Strengthen. If strengthenS is applied to a substitution with an outermost Strengthen constructor, then the "error message" of that constructor is discarded in favour of the Impossible argument of this function.

listS :: EndoSubst a => [(Int, a)] -> Substitution' a Source #

lookupS (listS [(x0,t0)..(xn,tn)]) xi = ti, assuming x0 < .. < xn.

raiseFromS :: Nat -> Nat -> Substitution' a Source #

Γ, Ξ, Δ ⊢ raiseFromS |Δ| |Ξ| : Γ, Δ

Functions on abstractions

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

Instantiate an abstraction. Strict in the term.

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

Instantiate an abstraction. Lazy in the term, which allow it to be IMPOSSIBLE in the case where the variable shouldn't be used but we cannot use noabsApp. Used in Apply.

noabsApp :: Subst a => Impossible -> Abs a -> a Source #

Instantiate an abstraction that doesn't use its argument.

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

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

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

underAbs :: Subst 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 :: TermSubst a => Int -> (a -> Term -> Term) -> a -> Term -> Term Source #

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