Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Substitute

Contents

Orphan instances

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

pattern LargeSort :: Univ -> Integer -> SizeOfSort
pattern SmallSort :: Univ -> SizeOfSort
absV :: Dom a -> ArgName -> TelV a -> TelV a
abstractArgs :: Abstract a => Args -> a -> a
applyNLPatSubst :: TermSubst a => Substitution' NLPat -> a -> a
applyNLSubstToDom :: SubstWith NLPat a => Substitution' NLPat -> Dom a -> Dom a
applyPatSubst :: TermSubst a => PatternSubstitution -> a -> a
applySubstTerm :: (Coercible t Term, EndoSubst t, Apply t) => Substitution' t -> t -> t
applyTermE :: (Coercible Term t, Apply t, EndoSubst t) => (Empty -> Term -> Elims -> Term) -> t -> Elims -> t
argToDontCare :: Arg Term -> Term
bindsToTel :: [Name] -> Dom Type -> ListTel
bindsToTel' :: (Name -> a) -> [Name] -> Dom Type -> ListTel' a
bindsToTel'1 :: (Name -> a) -> List1 Name -> Dom Type -> ListTel' a
bindsToTel1 :: List1 Name -> Dom Type -> ListTel
canProject :: QName -> Term -> Maybe (Arg Term)
compiledClauseBody :: Clause -> Maybe Term
conApp :: (Coercible t Term, Apply t) => (Empty -> Term -> Elims -> Term) -> ConHead -> ConInfo -> Elims -> Elims -> Term
defApp :: QName -> Elims -> Elims -> Term
domFromNamedArgName :: NamedArg Name -> Dom ()
fromPatternSubstitution :: PatternSubstitution -> Substitution
funSort :: Sort -> Sort -> Sort
funSort' :: Sort -> Sort -> Either Blocker Sort
isSmallSort :: Sort -> Bool
lamView :: Term -> ([Arg ArgName], Term)
levelLub :: Level -> Level -> Level
levelMax :: Integer -> [PlusLevel] -> Level
levelTm :: Level -> Term
mkLam :: Arg ArgName -> Term -> Term
mkPi :: Dom (ArgName, Type) -> Type -> Type
mkPiSort :: Dom Type -> Abs Type -> Sort
namedBindsToTel :: [NamedArg Name] -> Type -> Telescope
namedBindsToTel1 :: List1 (NamedArg Name) -> Type -> Telescope
namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern]
piApply :: Type -> Args -> Type
piSort :: Dom Term -> Sort -> Abs Sort -> Sort
piSort' :: Dom Term -> Sort -> Abs Sort -> Either Blocker Sort
projDropParsApply :: Projection -> ProjOrigin -> Relevance -> Args -> Term
relToDontCare :: LensRelevance a => a -> Term -> Term
renameP :: Subst a => Impossible -> Permutation -> a -> a
renaming :: DeBruijn a => Impossible -> Permutation -> Substitution' a
renamingR :: DeBruijn a => Permutation -> Substitution' a
sizeOfSort :: Sort -> Either Blocker SizeOfSort
sort :: Sort -> Type
ssort :: Level -> Type
telVars :: Int -> Telescope -> [Arg DeBruijnPattern]
telView' :: Type -> TelView
telView'UpTo :: Int -> Type -> TelView
teleLam :: Telescope -> Term -> Term
telePi :: Telescope -> Type -> Type
telePi' :: (Abs Type -> Abs Type) -> Telescope -> Type -> Type
telePiVisible :: Telescope -> Type -> Type
telePi_ :: Telescope -> Type -> Type
typeArgsWithTel :: Telescope -> [Term] -> Maybe [Dom Type]
univSort :: Sort -> Sort
univSort' :: Sort -> Either Blocker Sort
unlamView :: [Arg ArgName] -> Term -> Term
usePatOrigin :: PatOrigin -> Pattern' a -> Pattern' a
usePatternInfo :: PatternInfo -> Pattern' a -> Pattern' a
data SizeOfSort = SizeOfSort {
- szSortUniv :: Univ
- szSortSize :: Integer
}
data TelV a = TelV {
- theTel :: Tele (Dom a)
- theCore :: a
}
type TelView = TelV Type
class TeleNoAbs a where
- teleNoAbs :: a -> Term -> Term
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

pattern LargeSort :: Univ -> Integer -> SizeOfSort Source #

pattern SmallSort :: Univ -> SizeOfSort Source #

absV :: Dom a -> ArgName -> TelV a -> TelV a Source #

Add given binding to the front of the telescope.

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

applyNLPatSubst :: TermSubst a => Substitution' NLPat -> a -> a Source #

applyNLSubstToDom :: SubstWith NLPat a => Substitution' NLPat -> Dom a -> Dom a Source #

applyPatSubst :: TermSubst a => PatternSubstitution -> a -> a Source #

applySubstTerm :: (Coercible t Term, EndoSubst t, Apply t) => Substitution' t -> t -> t Source #

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.

argToDontCare :: Arg Term -> Term Source #

bindsToTel :: [Name] -> Dom Type -> ListTel Source #

bindsToTel' :: (Name -> a) -> [Name] -> Dom Type -> ListTel' a Source #

Turn a typed binding (x1 .. xn : A) into a telescope.

bindsToTel'1 :: (Name -> a) -> List1 Name -> Dom Type -> ListTel' a Source #

bindsToTel1 :: List1 Name -> Dom Type -> ListTel Source #

canProject :: QName -> Term -> Maybe (Arg Term) Source #

If v is a record or constructed value, canProject f v returns its field f.

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.

conApp :: (Coercible t Term, Apply t) => (Empty -> Term -> Elims -> Term) -> ConHead -> ConInfo -> Elims -> Elims -> Term Source #

Eliminate a constructed term.

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.

domFromNamedArgName :: NamedArg Name -> Dom () Source #

fromPatternSubstitution :: PatternSubstitution -> Substitution Source #

funSort :: Sort -> Sort -> Sort 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.

isSmallSort :: Sort -> Bool Source #

lamView :: Term -> ([Arg ArgName], Term) Source #

levelLub :: Level -> Level -> Level Source #

Given two levels a and b, compute a ⊔ b and return its canonical form.

levelMax :: Integer -> [PlusLevel] -> Level Source #

levelTm :: Level -> Term Source #

mkLam :: Arg ArgName -> Term -> Term Source #

mkPi :: Dom (ArgName, Type) -> Type -> Type Source #

mkPi dom t = telePi (telFromList [dom]) t

mkPiSort :: Dom Type -> Abs Type -> Sort Source #

namedBindsToTel :: [NamedArg Name] -> Type -> Telescope Source #

Turn a typed binding (x1 .. xn : A) into a telescope.

namedBindsToTel1 :: List1 (NamedArg Name) -> Type -> Telescope Source #

namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern] 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.

piSort :: Dom Term -> Sort -> Abs Sort -> Sort Source #

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

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.

relToDontCare :: LensRelevance a => a -> Term -> Term Source #

renameP :: Subst a => Impossible -> Permutation -> a -> a Source #

The permutation should permute the corresponding context. (right-to-left list)

renaming :: DeBruijn a => Impossible -> Permutation -> Substitution' a Source #

If permute π : [a]Γ -> [a]Δ, then applySubst (renaming _ π) : Term Γ -> Term Δ

renamingR :: DeBruijn a => Permutation -> Substitution' a Source #

If permute π : [a]Γ -> [a]Δ, then applySubst (renamingR π) : Term Δ -> Term Γ

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.

sort :: Sort -> Type Source #

ssort :: Level -> Type Source #

telVars :: Int -> Telescope -> [Arg DeBruijnPattern] Source #

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.

teleLam :: Telescope -> Term -> Term Source #

Abstract over a telescope in a term, producing lambdas. Dumb abstraction: Always produces Abs, never NoAbs.

The implementation is sound because Telescope does not use NoAbs.

telePi :: Telescope -> Type -> Type Source #

Uses free variable analysis to introduce NoAbs bindings.

telePi' :: (Abs Type -> Abs Type) -> Telescope -> Type -> Type Source #

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!

telePi_ :: Telescope -> Type -> Type Source #

Everything will be an Abs.

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.

univSort :: Sort -> Sort Source #

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

unlamView :: [Arg ArgName] -> Term -> Term Source #

usePatOrigin :: PatOrigin -> Pattern' a -> Pattern' a Source #

usePatternInfo :: PatternInfo -> Pattern' a -> Pattern' a Source #

data SizeOfSort Source #

A sort can either be small (Set l, Prop l, Size, ...) or large (Setω n).

Constructors

SizeOfSort
Fields szSortUniv :: Univ szSortSize :: Integer

data TelV a Source #

Constructors

TelV
Fields theTel :: Tele (Dom a) theCore :: a

Instances

Instances details

Functor TelV Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods fmap :: (a -> b) -> TelV a -> TelV b # (<$) :: a -> TelV b -> TelV a #
Show a => Show (TelV a) Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods showsPrec :: Int -> TelV a -> ShowS # show :: TelV a -> String # showList :: [TelV a] -> ShowS #
(TermSubst a, Eq a) => Eq (TelV a) Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: TelV a -> TelV a -> Bool # (/=) :: TelV a -> TelV a -> Bool #
(TermSubst a, Ord a) => Ord (TelV a) Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods compare :: TelV a -> TelV a -> Ordering # (<) :: TelV a -> TelV a -> Bool # (<=) :: TelV a -> TelV a -> Bool # (>) :: TelV a -> TelV a -> Bool # (>=) :: TelV a -> TelV a -> Bool # max :: TelV a -> TelV a -> TelV a # min :: TelV a -> TelV a -> TelV a #

type TelView = TelV Type Source #

class TeleNoAbs a where Source #

Performs void (noAbs) abstraction over telescope.

Methods

teleNoAbs :: a -> Term -> Term Source #

Instances

Instances details

TeleNoAbs ListTel Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods teleNoAbs :: ListTel -> Term -> Term Source #
TeleNoAbs Telescope Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods teleNoAbs :: Telescope -> Term -> Term Source #

module Agda.TypeChecking.Substitute.Class

module Agda.TypeChecking.Substitute.DeBruijn

data Substitution' a Source #

Substitutions.

Constructors

IdS	Identity substitution. `Γ ⊢ IdS : Γ`
EmptyS Impossible	Empty substitution, lifts from the empty context. First argument is `IMPOSSIBLE`. Apply this to closed terms you want to use in a non-empty context. `Γ ⊢ EmptyS : ()`
a :# (Substitution' a) infixr 4	Substitution extension, ``cons'`. `Γ ⊢ u : Aρ Γ ⊢ ρ : Δ ---------------------- Γ ⊢ u :# ρ : Δ, A`
Strengthen Impossible !Int (Substitution' a)	Strengthening substitution. First argument is `IMPOSSIBLE`. In `'Strengthen err n ρ` the number `n` must be non-negative. This substitution should only be applied to values `t` for which none of the variables `0` up to `n - 1` are free in `t[ρ]`, and in that case `n` is subtracted from all free de Bruijn indices in `t[ρ]`. Γ ⊢ ρ : Δ \|Θ\| = n --------------------------- Γ ⊢ Strengthen n ρ : Δ, Θ @
Wk !Int (Substitution' a)	Weakening substitution, lifts to an extended context. `Γ ⊢ ρ : Δ ------------------- Γ, Ψ ⊢ Wk \|Ψ\| ρ : Δ`
Lift !Int (Substitution' a)	Lifting substitution. Use this to go under a binder. `Lift 1 ρ == var 0 :# Wk 1 ρ`. `Γ ⊢ ρ : Δ ------------------------- Γ, Ψρ ⊢ Lift \|Ψ\| ρ : Δ, Ψ`

Instances

Instances details

KillRange Substitution Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Substitution Source #

InstantiateFull Substitution Source #

Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Substitution -> ReduceM Substitution Source #

Functor Substitution' Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

fmap :: (a -> b) -> Substitution' a -> Substitution' b #

(<$) :: a -> Substitution' b -> Substitution' a #

Foldable Substitution' Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

fold :: Monoid m => Substitution' m -> m #

foldMap :: Monoid m => (a -> m) -> Substitution' a -> m #

foldMap' :: Monoid m => (a -> m) -> Substitution' a -> m #

foldr :: (a -> b -> b) -> b -> Substitution' a -> b #

foldr' :: (a -> b -> b) -> b -> Substitution' a -> b #

foldl :: (b -> a -> b) -> b -> Substitution' a -> b #

foldl' :: (b -> a -> b) -> b -> Substitution' a -> b #

foldr1 :: (a -> a -> a) -> Substitution' a -> a #

foldl1 :: (a -> a -> a) -> Substitution' a -> a #

toList :: Substitution' a -> [a] #

null :: Substitution' a -> Bool #

length :: Substitution' a -> Int #

elem :: Eq a => a -> Substitution' a -> Bool #

maximum :: Ord a => Substitution' a -> a #

minimum :: Ord a => Substitution' a -> a #

sum :: Num a => Substitution' a -> a #

product :: Num a => Substitution' a -> a #

Traversable Substitution' Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

traverse :: Applicative f => (a -> f b) -> Substitution' a -> f (Substitution' b) #

sequenceA :: Applicative f => Substitution' (f a) -> f (Substitution' a) #

mapM :: Monad m => (a -> m b) -> Substitution' a -> m (Substitution' b) #

sequence :: Monad m => Substitution' (m a) -> m (Substitution' a) #

Eq Substitution Source #

Instance details

Defined in Agda.TypeChecking.Substitute

Methods

(==) :: Substitution -> Substitution -> Bool #

(/=) :: Substitution -> Substitution -> Bool #

Ord Substitution Source #

Instance details

Defined in Agda.TypeChecking.Substitute

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 #

Pretty a => Pretty (Substitution' a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

pretty :: Substitution' a -> Doc Source #

prettyPrec :: Int -> Substitution' a -> Doc Source #

prettyList :: [Substitution' a] -> Doc Source #

TermSize a => TermSize (Substitution' a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

termSize :: Substitution' a -> Int Source #

tsize :: Substitution' a -> Sum Int Source #

NamesIn a => NamesIn (Substitution' a) Source #

Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Substitution' a -> m Source #

(Pretty a, PrettyTCM a, EndoSubst a) => PrettyTCM (Substitution' a) Source #

Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Substitution' a -> m Doc Source #

EmbPrj a => EmbPrj (Substitution' a) Source #

Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Substitution' a -> S Word32 Source #

icod_ :: Substitution' a -> S Word32 Source #

value :: Word32 -> R (Substitution' a) Source #

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

Methods

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

Null (Substitution' a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

empty :: Substitution' a Source #

null :: Substitution' a -> Bool Source #

NFData a => NFData (Substitution' a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Substitution' a -> () #

Generic (Substitution' a) Source #

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep (Substitution' a)

Instance details

Defined in Agda.Syntax.Internal

Methods

from :: Substitution' a -> Rep (Substitution' a) x #

to :: Rep (Substitution' a) x -> Substitution' a #

Show a => Show (Substitution' a) Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

showsPrec :: Int -> Substitution' a -> ShowS #

show :: Substitution' a -> String #

showList :: [Substitution' a] -> ShowS #

type SubstArg (Substitution' a) Source #

Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg (Substitution' a) = a

type Rep (Substitution' a) Source #

Instance details

Defined in Agda.Syntax.Internal

type Substitution = Substitution' Term Source #

Orphan instances

Abstract Clause Source #

Instance details

Methods

abstract :: Telescope -> Clause -> Clause Source #

Abstract Sort Source #

Instance details

Methods

abstract :: Telescope -> Sort -> Sort Source #

Abstract Telescope Source #

Instance details

Methods

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

Abstract Term Source #

Instance details

Methods

abstract :: Telescope -> Term -> Term Source #

Abstract Type Source #

Instance details

Methods

abstract :: Telescope -> Type -> Type Source #

Abstract CompiledClauses Source #

Instance details

Methods

abstract :: Telescope -> CompiledClauses -> CompiledClauses Source #

Abstract Definition Source #

Instance details

Methods

abstract :: Telescope -> Definition -> Definition Source #

Abstract Defn Source #

Instance details

Methods

abstract :: Telescope -> Defn -> Defn Source #

Abstract FunctionInverse Source #

Instance details

Methods

abstract :: Telescope -> FunctionInverse -> FunctionInverse Source #

Abstract NumGeneralizableArgs Source #

Instance details

Methods

abstract :: Telescope -> NumGeneralizableArgs -> NumGeneralizableArgs Source #

Abstract PrimFun Source #

Instance details

Methods

abstract :: Telescope -> PrimFun -> PrimFun Source #

Abstract ProjLams Source #

Instance details

Methods

abstract :: Telescope -> ProjLams -> ProjLams Source #

Abstract Projection Source #

Instance details

Methods

abstract :: Telescope -> Projection -> Projection 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

Methods

abstract :: Telescope -> RewriteRule -> RewriteRule Source #

Abstract System Source #

Instance details

Methods

abstract :: Telescope -> System -> System Source #

Abstract Permutation Source #

Instance details

Methods

abstract :: Telescope -> Permutation -> Permutation Source #

Apply BraveTerm Source #

Instance details

Methods

apply :: BraveTerm -> Args -> BraveTerm Source #

applyE :: BraveTerm -> Elims -> BraveTerm Source #

Apply Clause Source #

Instance details

Methods

apply :: Clause -> Args -> Clause Source #

applyE :: Clause -> Elims -> Clause Source #

Apply Sort Source #

Instance details

Methods

apply :: Sort -> Args -> Sort Source #

applyE :: Sort -> Elims -> Sort Source #

Apply Term Source #

Instance details

Methods

apply :: Term -> Args -> Term Source #

applyE :: Term -> Elims -> Term Source #

Apply CompiledClauses Source #

Instance details

Methods

apply :: CompiledClauses -> Args -> CompiledClauses Source #

applyE :: CompiledClauses -> Elims -> CompiledClauses Source #

Apply Definition Source #

Instance details

Methods

apply :: Definition -> Args -> Definition Source #

applyE :: Definition -> Elims -> Definition Source #

Apply Defn Source #

Instance details

Methods

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

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

Apply DisplayTerm Source #

Instance details

Methods

apply :: DisplayTerm -> Args -> DisplayTerm Source #

applyE :: DisplayTerm -> Elims -> DisplayTerm Source #

Apply ExtLamInfo Source #

Instance details

Methods

apply :: ExtLamInfo -> Args -> ExtLamInfo Source #

applyE :: ExtLamInfo -> Elims -> ExtLamInfo Source #

Apply FunctionInverse Source #

Instance details

Methods

apply :: FunctionInverse -> Args -> FunctionInverse Source #

applyE :: FunctionInverse -> Elims -> FunctionInverse Source #

Apply NumGeneralizableArgs Source #

Instance details

Methods

apply :: NumGeneralizableArgs -> Args -> NumGeneralizableArgs Source #

applyE :: NumGeneralizableArgs -> Elims -> NumGeneralizableArgs Source #

Apply PrimFun Source #

Instance details

Methods

apply :: PrimFun -> Args -> PrimFun Source #

applyE :: PrimFun -> Elims -> PrimFun Source #

Apply ProjLams Source #

Instance details

Methods

apply :: ProjLams -> Args -> ProjLams Source #

applyE :: ProjLams -> Elims -> ProjLams Source #

Apply Projection Source #

Instance details

Methods

apply :: Projection -> Args -> Projection Source #

applyE :: Projection -> Elims -> Projection Source #

Apply RewriteRule Source #

Instance details

Methods

apply :: RewriteRule -> Args -> RewriteRule Source #

applyE :: RewriteRule -> Elims -> RewriteRule Source #

Apply System Source #

Instance details

Methods

apply :: System -> Args -> System Source #

applyE :: System -> Elims -> System Source #

Apply Permutation Source #

Instance details

Methods

apply :: Permutation -> Args -> Permutation Source #

applyE :: Permutation -> Elims -> Permutation Source #

Subst ProblemEq Source #

Instance details

Associated Types

type SubstArg ProblemEq
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg ProblemEq = Term

Methods

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

Subst Name Source #

Instance details

Associated Types

type SubstArg Name
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Name = Term

Methods

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

Subst BraveTerm Source #

Instance details

Associated Types

type SubstArg BraveTerm
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg BraveTerm = BraveTerm

Methods

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

Subst ConPatternInfo Source #

Instance details

Associated Types

type SubstArg ConPatternInfo
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg ConPatternInfo = Term

Methods

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

Subst DeBruijnPattern Source #

Instance details

Associated Types

type SubstArg DeBruijnPattern
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg DeBruijnPattern = DeBruijnPattern

Methods

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

Subst EqualityTypeData Source #

Instance details

Associated Types

type SubstArg EqualityTypeData
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg EqualityTypeData = Term

Methods

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

Subst EqualityView Source #

Instance details

Associated Types

type SubstArg EqualityView
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg EqualityView = Term

Methods

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

Subst Pattern Source #

Instance details

Associated Types

type SubstArg Pattern
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Pattern = Term

Methods

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

Subst Term Source #

Instance details

Associated Types

type SubstArg Term
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Term = Term

Methods

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

Subst Range Source #

Instance details

Associated Types

type SubstArg Range
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Range = Term

Methods

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

Subst Candidate Source #

Instance details

Associated Types

type SubstArg Candidate
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Candidate = Term

Methods

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

Subst CompareAs Source #

Instance details

Associated Types

type SubstArg CompareAs
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg CompareAs = Term

Methods

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

Subst Constraint Source #

Instance details

Associated Types

type SubstArg Constraint
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg Constraint = Term

Methods

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

Subst DisplayForm Source #

Instance details

Associated Types

type SubstArg DisplayForm
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg DisplayForm = Term

Methods

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

Subst DisplayTerm Source #

Instance details

Associated Types

type SubstArg DisplayTerm
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg DisplayTerm = Term

Methods

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

Subst LetBinding Source #

Instance details

Associated Types

type SubstArg LetBinding
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg LetBinding = Term

Methods

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

Subst NLPSort Source #

Instance details

Associated Types

type SubstArg NLPSort
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg NLPSort = NLPat

Methods

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

Subst NLPType Source #

Instance details

Associated Types

type SubstArg NLPType
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg NLPType = NLPat

Methods

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

Subst NLPat Source #

Instance details

Associated Types

type SubstArg NLPat
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg NLPat = NLPat

Methods

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

Subst RewriteRule Source #

Instance details

Associated Types

type SubstArg RewriteRule
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg RewriteRule = NLPat

Methods

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

Subst ContextEntry Source #

Instance details

Associated Types

type SubstArg ContextEntry
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg ContextEntry = Term

Methods

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

Subst () Source #

Instance details

Associated Types

type SubstArg ()
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg () = Term

Methods

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

DeBruijn BraveTerm Source #

Instance details

Methods

deBruijnVar :: Int -> BraveTerm Source #

deBruijnNamedVar :: String -> Int -> BraveTerm Source #

deBruijnView :: BraveTerm -> Maybe Int Source #

DeBruijn NLPat Source #

Instance details

Methods

deBruijnVar :: Int -> NLPat Source #

deBruijnNamedVar :: String -> Int -> NLPat Source #

deBruijnView :: NLPat -> Maybe Int Source #

Eq Level Source #

Instance details

Methods

(==) :: Level -> Level -> Bool #

(/=) :: Level -> Level -> Bool #

Eq NotBlocked Source #

Instance details

Methods

(==) :: NotBlocked -> NotBlocked -> Bool #

(/=) :: NotBlocked -> NotBlocked -> Bool #

Eq PlusLevel Source #

Instance details

Methods

(==) :: PlusLevel -> PlusLevel -> Bool #

(/=) :: PlusLevel -> PlusLevel -> Bool #

Eq Sort Source #

Instance details

Methods

(==) :: Sort -> Sort -> Bool #

(/=) :: Sort -> Sort -> Bool #

Eq Substitution Source #

Instance details

Methods

(==) :: Substitution -> Substitution -> Bool #

(/=) :: Substitution -> Substitution -> Bool #

Eq Term Source #

Syntactic Term equality, ignores stuff below DontCare and sharing.

Instance details

Methods

(==) :: Term -> Term -> Bool #

(/=) :: Term -> Term -> Bool #

Eq Candidate Source #

Instance details

Methods

(==) :: Candidate -> Candidate -> Bool #

(/=) :: Candidate -> Candidate -> Bool #

Eq CandidateKind Source #

Instance details

Methods

(==) :: CandidateKind -> CandidateKind -> Bool #

(/=) :: CandidateKind -> CandidateKind -> Bool #

Eq Section Source #

Instance details

Methods

(==) :: Section -> Section -> Bool #

(/=) :: Section -> Section -> Bool #

Ord Level Source #

Instance details

Methods

compare :: Level -> Level -> Ordering #

(<) :: Level -> Level -> Bool #

(<=) :: Level -> Level -> Bool #

(>) :: Level -> Level -> Bool #

(>=) :: Level -> Level -> Bool #

max :: Level -> Level -> Level #

min :: Level -> Level -> Level #

Ord PlusLevel Source #

Instance details

Methods

compare :: PlusLevel -> PlusLevel -> Ordering #

(<) :: PlusLevel -> PlusLevel -> Bool #

(<=) :: PlusLevel -> PlusLevel -> Bool #

(>) :: PlusLevel -> PlusLevel -> Bool #

(>=) :: PlusLevel -> PlusLevel -> Bool #

max :: PlusLevel -> PlusLevel -> PlusLevel #

min :: PlusLevel -> PlusLevel -> PlusLevel #

Ord Sort Source #

Instance details

Methods

compare :: Sort -> Sort -> Ordering #

(<) :: Sort -> Sort -> Bool #

(<=) :: Sort -> Sort -> Bool #

(>) :: Sort -> Sort -> Bool #

(>=) :: Sort -> Sort -> Bool #

max :: Sort -> Sort -> Sort #

min :: Sort -> Sort -> Sort #

Ord Substitution Source #

Instance details

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 #

Instance details

Methods

compare :: Term -> Term -> Ordering #

(<) :: Term -> Term -> Bool #

(<=) :: Term -> Term -> Bool #

(>) :: Term -> Term -> Bool #

(>=) :: Term -> Term -> Bool #

max :: Term -> Term -> Term #

min :: Term -> Term -> Term #

Ord Candidate Source #

Instance details

Methods

compare :: Candidate -> Candidate -> Ordering #

(<) :: Candidate -> Candidate -> Bool #

(<=) :: Candidate -> Candidate -> Bool #

(>) :: Candidate -> Candidate -> Bool #

(>=) :: Candidate -> Candidate -> Bool #

max :: Candidate -> Candidate -> Candidate #

min :: Candidate -> Candidate -> Candidate #

Ord CandidateKind Source #

Instance details

Methods

compare :: CandidateKind -> CandidateKind -> Ordering #

(<) :: CandidateKind -> CandidateKind -> Bool #

(<=) :: CandidateKind -> CandidateKind -> Bool #

(>) :: CandidateKind -> CandidateKind -> Bool #

(>=) :: CandidateKind -> CandidateKind -> Bool #

max :: CandidateKind -> CandidateKind -> CandidateKind #

min :: CandidateKind -> CandidateKind -> CandidateKind #

Abstract a => Abstract (Case a) Source #

Instance details

Methods

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

Abstract a => Abstract (WithArity a) Source #

Instance details

Methods

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

DoDrop a => Abstract (Drop a) Source #

Instance details

Methods

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

Abstract t => Abstract (Maybe t) Source #

Instance details

Methods

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

Abstract [Polarity] Source #

Instance details

Methods

abstract :: Telescope -> [Polarity] -> [Polarity] Source #

Abstract [Occurrence] Source #

Instance details

Methods

abstract :: Telescope -> [Occurrence] -> [Occurrence] Source #

Abstract t => Abstract [t] Source #

Instance details

Methods

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

Apply t => Apply (Blocked t) Source #

Instance details

Methods

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

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

TermSubst a => Apply (Tele a) Source #

Instance details

Methods

apply :: Tele a -> Args -> Tele a Source #

applyE :: Tele a -> Elims -> Tele a Source #

Apply a => Apply (Case a) Source #

Instance details

Methods

apply :: Case a -> Args -> Case a Source #

applyE :: Case a -> Elims -> Case a Source #

Apply a => Apply (WithArity a) Source #

Instance details

Methods

apply :: WithArity a -> Args -> WithArity a Source #

applyE :: WithArity a -> Elims -> WithArity a Source #

DoDrop a => Apply (Drop a) Source #

Instance details

Methods

apply :: Drop a -> Args -> Drop a Source #

applyE :: Drop a -> Elims -> Drop a Source #

Apply t => Apply (Maybe t) Source #

Instance details

Methods

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

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

Apply t => Apply (Maybe t) Source #

Instance details

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

Methods

apply :: [NamedArg (Pattern' a)] -> Args -> [NamedArg (Pattern' a)] Source #

applyE :: [NamedArg (Pattern' a)] -> Elims -> [NamedArg (Pattern' a)] Source #

Apply [Polarity] Source #

Instance details

Methods

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

applyE :: [Polarity] -> Elims -> [Polarity] Source #

Apply [Occurrence] Source #

Instance details

Methods

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

applyE :: [Occurrence] -> Elims -> [Occurrence] Source #

Apply t => Apply [t] Source #

Instance details

Methods

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

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

Subst a => Subst (Arg a) Source #

Instance details

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

Associated Types

type SubstArg (WithHiding a)
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (WithHiding a) = SubstArg a

Methods

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

Subst a => Subst (Abs a) Source #

Instance details

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

Associated Types

type SubstArg (Blocked a)
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Blocked a) = SubstArg a

Methods

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

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

Instance details

Associated Types

type SubstArg (Level' a)
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Level' a) = SubstArg a

Methods

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

Subst a => Subst (PlusLevel' a) Source #

Instance details

Associated Types

type SubstArg (PlusLevel' a)
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (PlusLevel' a) = SubstArg a

Methods

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

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

Instance details

Associated Types

type SubstArg (Sort' a)
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Sort' a) = SubstArg a

Methods

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

EndoSubst a => Subst (Substitution' a) Source #

Instance details

Associated Types

type SubstArg (Substitution' a)
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Substitution' a) = a

Methods

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

Subst a => Subst (Tele a) Source #

Instance details

Associated Types

type SubstArg (Tele a)
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Tele a) = SubstArg a

Methods

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

Subst a => Subst (Elim' a) Source #

Instance details

Associated Types

type SubstArg (Elim' a)
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Elim' a) = SubstArg a

Methods

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

Subst a => Subst (List1 a) Source #

Instance details

Associated Types

type SubstArg (List1 a)
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (List1 a) = SubstArg a

Methods

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

Subst a => Subst (Maybe a) Source #

Instance details

Associated Types

type SubstArg (Maybe a)
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Maybe a) = SubstArg a

Methods

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

Subst a => Subst [a] Source #

Instance details

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 #

DeBruijn a => DeBruijn (Pattern' a) Source #

Instance details

Methods

deBruijnVar :: Int -> Pattern' a Source #

deBruijnNamedVar :: String -> Int -> Pattern' a Source #

deBruijnView :: Pattern' a -> Maybe Int 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.

Instance details

Methods

(==) :: Abs a -> Abs a -> Bool #

(/=) :: Abs a -> Abs a -> Bool #

Eq t => Eq (Blocked t) Source #

Instance details

Methods

(==) :: Blocked t -> Blocked t -> Bool #

(/=) :: Blocked t -> Blocked t -> Bool #

Eq a => Eq (Pattern' a) Source #

Instance details

Methods

(==) :: Pattern' a -> Pattern' a -> Bool #

(/=) :: Pattern' a -> Pattern' a -> Bool #

(Subst a, Eq a) => Eq (Tele a) Source #

Instance details

Methods

(==) :: Tele a -> Tele a -> Bool #

(/=) :: Tele a -> Tele a -> Bool #

Eq a => Eq (Type' a) Source #

Syntactic Type equality, ignores sort annotations.

Instance details

Methods

(==) :: Type' a -> Type' a -> Bool #

(/=) :: Type' a -> Type' a -> Bool #

(Subst a, Eq a) => Eq (Elim' a) Source #

Instance details

Methods

(==) :: Elim' a -> Elim' a -> Bool #

(/=) :: Elim' a -> Elim' a -> Bool #

(Subst a, Ord a) => Ord (Abs a) Source #

Instance details

Methods

compare :: Abs a -> Abs a -> Ordering #

(<) :: Abs a -> Abs a -> Bool #

(<=) :: Abs a -> Abs a -> Bool #

(>) :: Abs a -> Abs a -> Bool #

(>=) :: Abs a -> Abs a -> Bool #

max :: Abs a -> Abs a -> Abs a #

min :: Abs a -> Abs a -> Abs a #

Ord a => Ord (Dom a) Source #

Instance details

Methods

compare :: Dom a -> Dom a -> Ordering #

(<) :: Dom a -> Dom a -> Bool #

(<=) :: Dom a -> Dom a -> Bool #

(>) :: Dom a -> Dom a -> Bool #

(>=) :: Dom a -> Dom a -> Bool #

max :: Dom a -> Dom a -> Dom a #

min :: Dom a -> Dom a -> Dom a #

(Subst a, Ord a) => Ord (Tele a) Source #

Instance details

Methods

compare :: Tele a -> Tele a -> Ordering #

(<) :: Tele a -> Tele a -> Bool #

(<=) :: Tele a -> Tele a -> Bool #

(>) :: Tele a -> Tele a -> Bool #

(>=) :: Tele a -> Tele a -> Bool #

max :: Tele a -> Tele a -> Tele a #

min :: Tele a -> Tele a -> Tele a #

Ord a => Ord (Type' a) Source #

Instance details

Methods

compare :: Type' a -> Type' a -> Ordering #

(<) :: Type' a -> Type' a -> Bool #

(<=) :: Type' a -> Type' a -> Bool #

(>) :: Type' a -> Type' a -> Bool #

(>=) :: Type' a -> Type' a -> Bool #

max :: Type' a -> Type' a -> Type' a #

min :: Type' a -> Type' a -> Type' a #

(Subst a, Ord a) => Ord (Elim' a) Source #

Instance details

Methods

compare :: Elim' a -> Elim' a -> Ordering #

(<) :: Elim' a -> Elim' a -> Bool #

(<=) :: Elim' a -> Elim' a -> Bool #

(>) :: Elim' a -> Elim' a -> Bool #

(>=) :: Elim' a -> Elim' a -> Bool #

max :: Elim' a -> Elim' a -> Elim' a #

min :: Elim' a -> Elim' a -> Elim' a #

Abstract v => Abstract (Map k v) Source #

Instance details

Methods

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

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

Instance details

Methods

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

Apply v => Apply (Map k v) Source #

Instance details

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

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

Methods

apply :: (a, b) -> Args -> (a, b) Source #

applyE :: (a, b) -> Elims -> (a, b) Source #

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

Instance details

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

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

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 #

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

Instance details

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

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 #

(Apply a, Apply b, Apply c) => Apply (a, b, c) Source #

Instance details

Methods

apply :: (a, b, c) -> Args -> (a, b, c) Source #

applyE :: (a, b, c) -> Elims -> (a, b, c) Source #

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

Instance details

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

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 #