Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.TypeChecking.Substitute
Contents
Description
This module contains the definition of hereditary substitution and application operating on internal syntax which is in β-normal form (β including projection reductions).
Further, it contains auxiliary functions which rely on substitution but not on reduction.
Synopsis
- sort :: Sort -> Type
- renamingR :: DeBruijn a => Permutation -> Substitution' a
- data TelV a = TelV {}
- mkLam :: Arg ArgName -> Term -> Term
- funSort :: Sort -> Sort -> Sort
- renaming :: DeBruijn a => Impossible -> Permutation -> Substitution' a
- piSort :: Dom Term -> Sort -> Abs Sort -> Sort
- univSort :: Sort -> Sort
- mkPi :: Dom (ArgName, Type) -> Type -> Type
- lamView :: Term -> ([Arg ArgName], Term)
- applyTermE :: (Coercible Term t, Apply t, EndoSubst t) => (Empty -> Term -> Elims -> Term) -> t -> Elims -> t
- defApp :: QName -> Elims -> Elims -> Term
- conApp :: (Coercible t Term, Apply t) => (Empty -> Term -> Elims -> Term) -> ConHead -> ConInfo -> Elims -> Elims -> Term
- canProject :: QName -> Term -> Maybe (Arg Term)
- relToDontCare :: LensRelevance a => a -> Term -> Term
- argToDontCare :: Arg Term -> Term
- piApply :: Type -> Args -> Type
- applyNLPatSubst :: TermSubst a => Substitution' NLPat -> a -> a
- teleLam :: Telescope -> Term -> Term
- telePi_ :: Telescope -> Type -> Type
- namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern]
- telVars :: Int -> Telescope -> [Arg DeBruijnPattern]
- abstractArgs :: Abstract a => Args -> a -> a
- renameP :: Subst a => Impossible -> Permutation -> a -> a
- applySubstTerm :: (Coercible t Term, EndoSubst t, Apply t) => Substitution' t -> t -> t
- levelTm :: Level -> Term
- applyNLSubstToDom :: SubstWith NLPat a => Substitution' NLPat -> Dom a -> Dom a
- fromPatternSubstitution :: PatternSubstitution -> Substitution
- applyPatSubst :: TermSubst a => PatternSubstitution -> a -> a
- usePatOrigin :: PatOrigin -> Pattern' a -> Pattern' a
- usePatternInfo :: PatternInfo -> Pattern' a -> Pattern' a
- projDropParsApply :: Projection -> ProjOrigin -> Relevance -> Args -> Term
- type TelView = TelV Type
- telView' :: Type -> TelView
- telView'UpTo :: Int -> Type -> TelView
- absV :: Dom a -> ArgName -> TelV a -> TelV a
- bindsToTel' :: (Name -> a) -> [Name] -> Dom Type -> ListTel' a
- bindsToTel :: [Name] -> Dom Type -> ListTel
- bindsToTel'1 :: (Name -> a) -> List1 Name -> Dom Type -> ListTel' a
- bindsToTel1 :: List1 Name -> Dom Type -> ListTel
- namedBindsToTel :: [NamedArg Name] -> Type -> Telescope
- domFromNamedArgName :: NamedArg Name -> Dom ()
- namedBindsToTel1 :: List1 (NamedArg Name) -> Type -> Telescope
- mkPiSort :: Dom Type -> Abs Type -> Sort
- unlamView :: [Arg ArgName] -> Term -> Term
- telePi' :: (Abs Type -> Abs Type) -> Telescope -> Type -> Type
- telePi :: Telescope -> Type -> Type
- telePiVisible :: Telescope -> Type -> Type
- class TeleNoAbs a where
- typeArgsWithTel :: Telescope -> [Term] -> Maybe [Dom Type]
- compiledClauseBody :: Clause -> Maybe Term
- univSort' :: Sort -> Either Blocker Sort
- ssort :: Level -> Type
- data SizeOfSort = SizeOfSort {
- szSortUniv :: Univ
- szSortSize :: Integer
- pattern SmallSort :: Univ -> SizeOfSort
- pattern LargeSort :: Univ -> Integer -> SizeOfSort
- sizeOfSort :: Sort -> Either Blocker SizeOfSort
- isSmallSort :: Sort -> Bool
- funSort' :: Sort -> Sort -> Either Blocker Sort
- levelLub :: Level -> Level -> Level
- piSort' :: Dom Term -> Sort -> Abs Sort -> Either Blocker Sort
- levelMax :: Integer -> [PlusLevel] -> Level
- module Agda.TypeChecking.Substitute.Class
- module Agda.TypeChecking.Substitute.DeBruijn
- data Substitution' a
- = IdS
- | EmptyS Impossible
- | a :# (Substitution' a)
- | Strengthen Impossible !Int (Substitution' a)
- | Wk !Int (Substitution' a)
- | Lift !Int (Substitution' a)
- type Substitution = Substitution' Term
Documentation
renamingR :: DeBruijn a => Permutation -> Substitution' a Source #
If permute π : [a]Γ -> [a]Δ
, then applySubst (renamingR π) : Term Δ -> Term Γ
renaming :: DeBruijn a => Impossible -> Permutation -> Substitution' a Source #
If permute π : [a]Γ -> [a]Δ
, then applySubst (renaming _ π) : Term Γ -> Term Δ
applyTermE :: (Coercible Term t, Apply t, EndoSubst t) => (Empty -> Term -> Elims -> Term) -> t -> Elims -> t Source #
Apply Elims
while using the given function to report ill-typed
redexes.
Recursive calls for applyE
and applySubst
happen at type t
to
propagate the same strategy to subtrees.
defApp :: QName -> Elims -> Elims -> Term Source #
defApp f us vs
applies Def f us
to further arguments vs
,
eliminating top projection redexes.
If us
is not empty, we cannot have a projection redex, since
the record argument is the first one.
conApp :: (Coercible t Term, Apply t) => (Empty -> Term -> Elims -> Term) -> ConHead -> ConInfo -> Elims -> Elims -> Term Source #
Eliminate a constructed term.
canProject :: QName -> Term -> Maybe (Arg Term) Source #
If v
is a record or constructed value, canProject f v
returns its field f
.
relToDontCare :: LensRelevance a => a -> Term -> Term Source #
piApply :: Type -> Args -> Type Source #
(x:A)->B(x) piApply
[u] = B(u)
Precondition: The type must contain the right number of pis without having to perform any reduction.
piApply
is potentially unsafe, the monadic piApplyM
is preferable.
applyNLPatSubst :: TermSubst a => Substitution' NLPat -> a -> a Source #
namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern] Source #
abstractArgs :: Abstract a => Args -> a -> a Source #
renameP :: Subst a => Impossible -> Permutation -> a -> a Source #
The permutation should permute the corresponding context. (right-to-left list)
applySubstTerm :: (Coercible t Term, EndoSubst t, Apply t) => Substitution' t -> t -> t Source #
applyNLSubstToDom :: SubstWith NLPat a => Substitution' NLPat -> Dom a -> Dom a Source #
applyPatSubst :: TermSubst a => PatternSubstitution -> a -> a Source #
usePatternInfo :: PatternInfo -> Pattern' a -> Pattern' a Source #
projDropParsApply :: Projection -> ProjOrigin -> Relevance -> Args -> Term Source #
projDropParsApply proj o args =projDropPars
proj o `apply'
args
This function is an optimization, saving us from construction lambdas we immediately remove through application.
telView' :: Type -> TelView Source #
Takes off all exposed function domains from the given type.
This means that it does not reduce to expose Pi
-types.
telView'UpTo :: Int -> Type -> TelView Source #
telView'UpTo n t
takes off the first n
exposed function types of t
.
Takes off all (exposed ones) if n < 0
.
absV :: Dom a -> ArgName -> TelV a -> TelV a Source #
Add given binding to the front of the telescope.
bindsToTel' :: (Name -> a) -> [Name] -> Dom Type -> ListTel' a Source #
Turn a typed binding (x1 .. xn : A)
into a telescope.
namedBindsToTel :: [NamedArg Name] -> Type -> Telescope Source #
Turn a typed binding (x1 .. xn : A)
into a telescope.
telePi :: Telescope -> Type -> Type Source #
Uses free variable analysis to introduce NoAbs
bindings.
telePiVisible :: Telescope -> Type -> Type Source #
Only abstract the visible components of the telescope,
and all that bind variables. Everything will be an Abs
!
Caution: quadratic time!
typeArgsWithTel :: Telescope -> [Term] -> Maybe [Dom Type] Source #
Given arguments vs : tel
(vector typing), extract their individual types.
Returns Nothing
is tel
is not long enough.
compiledClauseBody :: Clause -> Maybe Term Source #
In compiled clauses, the variables in the clause body are relative to the pattern variables (including dot patterns) instead of the clause telescope.
univSort' :: Sort -> Either Blocker Sort Source #
univSort' univInf s
gets the next higher sort of s
, if it is
known (i.e. it is not just UnivSort s
).
Precondition: s
is reduced
data SizeOfSort Source #
A sort can either be small (Set l, Prop l, Size, ...) or large (Setω n).
Constructors
SizeOfSort | |
Fields
|
pattern SmallSort :: Univ -> SizeOfSort Source #
sizeOfSort :: Sort -> Either Blocker SizeOfSort Source #
Returns Left blocker
for unknown (blocked) sorts, and otherwise
returns Right s
where s
indicates the size and fibrancy.
isSmallSort :: Sort -> Bool Source #
funSort' :: Sort -> Sort -> Either Blocker Sort Source #
Compute the sort of a function type from the sorts of its domain and codomain.
This function should only be called on reduced sorts,
since the LevelUniv
rules should only apply when the sort does not reduce to Set
.
levelLub :: Level -> Level -> Level Source #
Given two levels a
and b
, compute a ⊔ b
and return its
canonical form.
piSort' :: Dom Term -> Sort -> Abs Sort -> Either Blocker Sort Source #
Compute the sort of a pi type from the sorts of its domain
and codomain.
This function should only be called on reduced sorts, since the LevelUniv
rules should only apply when the sort doesn't reduce to Set
data Substitution' a Source #
Substitutions.
Constructors
IdS | Identity substitution.
|
EmptyS Impossible | Empty substitution, lifts from the empty context. First argument is |
a :# (Substitution' a) infixr 4 | Substitution extension, ` |
Strengthen Impossible !Int (Substitution' a) | Strengthening substitution. First argument is |
Wk !Int (Substitution' a) | Weakening substitution, lifts to an extended context.
|
Lift !Int (Substitution' a) | Lifting substitution. Use this to go under a binder.
|
Instances
type Substitution = Substitution' Term Source #
Orphan instances
Abstract Clause Source # | |||||
Abstract Sort Source # | |||||
Abstract Telescope Source # | |||||
Abstract Term Source # | |||||
Abstract Type Source # | |||||
Abstract CompiledClauses Source # | |||||
Methods abstract :: Telescope -> CompiledClauses -> CompiledClauses Source # | |||||
Abstract Definition Source # | |||||
Methods abstract :: Telescope -> Definition -> Definition Source # | |||||
Abstract Defn Source # | |||||
Abstract FunctionInverse Source # | |||||
Methods abstract :: Telescope -> FunctionInverse -> FunctionInverse Source # | |||||
Abstract NumGeneralizableArgs Source # | |||||
Methods abstract :: Telescope -> NumGeneralizableArgs -> NumGeneralizableArgs Source # | |||||
Abstract PrimFun Source # | |||||
Abstract ProjLams Source # | |||||
Abstract Projection Source # | |||||
Methods abstract :: Telescope -> Projection -> Projection Source # | |||||
Abstract RewriteRule Source # |
| ||||
Methods abstract :: Telescope -> RewriteRule -> RewriteRule Source # | |||||
Abstract System Source # | |||||
Abstract Permutation Source # | |||||
Methods abstract :: Telescope -> Permutation -> Permutation Source # | |||||
Apply BraveTerm Source # | |||||
Apply Clause Source # | |||||
Apply Sort Source # | |||||
Apply Term Source # | |||||
Apply CompiledClauses Source # | |||||
Methods apply :: CompiledClauses -> Args -> CompiledClauses Source # applyE :: CompiledClauses -> Elims -> CompiledClauses Source # | |||||
Apply Definition Source # | |||||
Methods apply :: Definition -> Args -> Definition Source # applyE :: Definition -> Elims -> Definition Source # | |||||
Apply Defn Source # | |||||
Apply DisplayTerm Source # | |||||
Methods apply :: DisplayTerm -> Args -> DisplayTerm Source # applyE :: DisplayTerm -> Elims -> DisplayTerm Source # | |||||
Apply ExtLamInfo Source # | |||||
Methods apply :: ExtLamInfo -> Args -> ExtLamInfo Source # applyE :: ExtLamInfo -> Elims -> ExtLamInfo Source # | |||||
Apply FunctionInverse Source # | |||||
Methods apply :: FunctionInverse -> Args -> FunctionInverse Source # applyE :: FunctionInverse -> Elims -> FunctionInverse Source # | |||||
Apply NumGeneralizableArgs Source # | |||||
Methods apply :: NumGeneralizableArgs -> Args -> NumGeneralizableArgs Source # applyE :: NumGeneralizableArgs -> Elims -> NumGeneralizableArgs Source # | |||||
Apply PrimFun Source # | |||||
Apply ProjLams Source # | |||||
Apply Projection Source # | |||||
Methods apply :: Projection -> Args -> Projection Source # applyE :: Projection -> Elims -> Projection Source # | |||||
Apply RewriteRule Source # | |||||
Methods apply :: RewriteRule -> Args -> RewriteRule Source # applyE :: RewriteRule -> Elims -> RewriteRule Source # | |||||
Apply System Source # | |||||
Apply Permutation Source # | |||||
Methods apply :: Permutation -> Args -> Permutation Source # applyE :: Permutation -> Elims -> Permutation Source # | |||||
Subst ProblemEq Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg ProblemEq) -> ProblemEq -> ProblemEq Source # | |||||
Subst Name Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg Name) -> Name -> Name Source # | |||||
Subst BraveTerm Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg BraveTerm) -> BraveTerm -> BraveTerm Source # | |||||
Subst ConPatternInfo Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg ConPatternInfo) -> ConPatternInfo -> ConPatternInfo Source # | |||||
Subst DeBruijnPattern Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg DeBruijnPattern) -> DeBruijnPattern -> DeBruijnPattern Source # | |||||
Subst EqualityTypeData Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg EqualityTypeData) -> EqualityTypeData -> EqualityTypeData Source # | |||||
Subst EqualityView Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg EqualityView) -> EqualityView -> EqualityView Source # | |||||
Subst Pattern Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg Pattern) -> Pattern -> Pattern Source # | |||||
Subst Term Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg Term) -> Term -> Term Source # | |||||
Subst Range Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg Range) -> Range -> Range Source # | |||||
Subst Candidate Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg Candidate) -> Candidate -> Candidate Source # | |||||
Subst CompareAs Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg CompareAs) -> CompareAs -> CompareAs Source # | |||||
Subst Constraint Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg Constraint) -> Constraint -> Constraint Source # | |||||
Subst DisplayForm Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg DisplayForm) -> DisplayForm -> DisplayForm Source # | |||||
Subst DisplayTerm Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg DisplayTerm) -> DisplayTerm -> DisplayTerm Source # | |||||
Subst LetBinding Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg LetBinding) -> LetBinding -> LetBinding Source # | |||||
Subst NLPSort Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg NLPSort) -> NLPSort -> NLPSort Source # | |||||
Subst NLPType Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg NLPType) -> NLPType -> NLPType Source # | |||||
Subst NLPat Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg NLPat) -> NLPat -> NLPat Source # | |||||
Subst RewriteRule Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg RewriteRule) -> RewriteRule -> RewriteRule Source # | |||||
Subst () Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg ()) -> () -> () Source # | |||||
DeBruijn BraveTerm Source # | |||||
DeBruijn NLPat Source # | |||||
Eq Level Source # | |||||
Eq NotBlocked Source # | |||||
Eq PlusLevel Source # | |||||
Eq Sort Source # | |||||
Eq Substitution Source # | |||||
Eq Term Source # | Syntactic | ||||
Eq Candidate Source # | |||||
Eq CandidateKind Source # | |||||
Methods (==) :: CandidateKind -> CandidateKind -> Bool # (/=) :: CandidateKind -> CandidateKind -> Bool # | |||||
Eq Section Source # | |||||
Ord Level Source # | |||||
Ord PlusLevel Source # | |||||
Ord Sort Source # | |||||
Ord Substitution Source # | |||||
Methods compare :: Substitution -> Substitution -> Ordering # (<) :: Substitution -> Substitution -> Bool # (<=) :: Substitution -> Substitution -> Bool # (>) :: Substitution -> Substitution -> Bool # (>=) :: Substitution -> Substitution -> Bool # max :: Substitution -> Substitution -> Substitution # min :: Substitution -> Substitution -> Substitution # | |||||
Ord Term Source # | |||||
Abstract a => Abstract (Case a) Source # | |||||
Abstract a => Abstract (WithArity a) Source # | |||||
DoDrop a => Abstract (Drop a) Source # | |||||
Abstract t => Abstract (Maybe t) Source # | |||||
Abstract [Polarity] Source # | |||||
Abstract [Occurrence] Source # | |||||
Methods abstract :: Telescope -> [Occurrence] -> [Occurrence] Source # | |||||
Abstract t => Abstract [t] Source # | |||||
Apply t => Apply (Blocked t) Source # | |||||
TermSubst a => Apply (Tele a) Source # | |||||
Apply a => Apply (Case a) Source # | |||||
Apply a => Apply (WithArity a) Source # | |||||
DoDrop a => Apply (Drop a) Source # | |||||
Apply t => Apply (Maybe t) Source # | |||||
Apply t => Apply (Maybe t) Source # | |||||
Apply [NamedArg (Pattern' a)] Source # | Make sure we only drop variable patterns. | ||||
Apply [Polarity] Source # | |||||
Apply [Occurrence] Source # | |||||
Methods apply :: [Occurrence] -> Args -> [Occurrence] Source # applyE :: [Occurrence] -> Elims -> [Occurrence] Source # | |||||
Apply t => Apply [t] Source # | |||||
Subst a => Subst (Arg a) Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg (Arg a)) -> Arg a -> Arg a Source # | |||||
Subst a => Subst (WithHiding a) Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg (WithHiding a)) -> WithHiding a -> WithHiding a Source # | |||||
Subst a => Subst (Abs a) Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg (Abs a)) -> Abs a -> Abs a Source # | |||||
Subst a => Subst (Blocked a) Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg (Blocked a)) -> Blocked a -> Blocked a Source # | |||||
Subst a => Subst (Level' a) Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg (Level' a)) -> Level' a -> Level' a Source # | |||||
Subst a => Subst (PlusLevel' a) Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg (PlusLevel' a)) -> PlusLevel' a -> PlusLevel' a Source # | |||||
(Coercible a Term, Subst a) => Subst (Sort' a) Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg (Sort' a)) -> Sort' a -> Sort' a Source # | |||||
EndoSubst a => Subst (Substitution' a) Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg (Substitution' a)) -> Substitution' a -> Substitution' a Source # | |||||
Subst a => Subst (Tele a) Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg (Tele a)) -> Tele a -> Tele a Source # | |||||
Subst a => Subst (Elim' a) Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg (Elim' a)) -> Elim' a -> Elim' a Source # | |||||
Subst a => Subst (Maybe a) Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg (Maybe a)) -> Maybe a -> Maybe a Source # | |||||
Subst a => Subst [a] Source # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg [a]) -> [a] -> [a] Source # | |||||
DeBruijn a => DeBruijn (Pattern' a) Source # | |||||
(Subst a, Eq a) => Eq (Abs a) Source # | Equality of binders relies on weakening which is a special case of renaming which is a special case of substitution. | ||||
Eq t => Eq (Blocked t) Source # | |||||
Eq a => Eq (Pattern' a) Source # | |||||
(Subst a, Eq a) => Eq (Tele a) Source # | |||||
Eq a => Eq (Type' a) Source # | Syntactic | ||||
(Subst a, Eq a) => Eq (Elim' a) Source # | |||||
(Subst a, Ord a) => Ord (Abs a) Source # | |||||
Ord a => Ord (Dom a) Source # | |||||
(Subst a, Ord a) => Ord (Tele a) Source # | |||||
Ord a => Ord (Type' a) Source # | |||||
(Subst a, Ord a) => Ord (Elim' a) Source # | |||||
Abstract v => Abstract (Map k v) Source # | |||||
Abstract v => Abstract (HashMap k v) Source # | |||||
Apply v => Apply (Map k v) Source # | |||||
Apply v => Apply (HashMap k v) Source # | |||||
(Apply a, Apply b) => Apply (a, b) Source # | |||||
Subst a => Subst (Named name a) Source # | |||||
Associated Types
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 # | |||||
Associated Types
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 # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg (Type'' a b)) -> Type'' a b -> Type'' a b Source # | |||||
(Ord k, Subst a) => Subst (Map k a) Source # | |||||
Associated Types
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 # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg (a, b)) -> (a, b) -> (a, b) Source # | |||||
(Apply a, Apply b, Apply c) => Apply (a, b, c) Source # | |||||
(Subst a, Subst b, Subst c, SubstArg a ~ SubstArg b, SubstArg b ~ SubstArg c) => Subst (a, b, c) Source # | |||||
Associated Types
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 # | |||||
Associated Types
Methods applySubst :: Substitution' (SubstArg (a, b, c, d)) -> (a, b, c, d) -> (a, b, c, d) Source # |