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

sort :: Sort -> Type
renamingR :: DeBruijn a => Permutation -> Substitution' a
data TelV a = TelV {
- theTel :: Tele (Dom a)
- theCore :: a
}
mkLam :: Arg ArgName -> Term -> Term
renaming :: DeBruijn a => Impossible -> Permutation -> Substitution' a
piSort :: Dom Term -> Sort -> Abs Sort -> Sort
funSort :: Sort -> 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
- teleNoAbs :: a -> Term -> Term
typeArgsWithTel :: Telescope -> [Term] -> Maybe [Dom Type]
compiledClauseBody :: Clause -> Maybe Term
univSort' :: Sort -> Either Blocker Sort
ssort :: Level -> Type
data SizeOfSort
- = SmallSort IsFibrant
- | LargeSort IsFibrant Integer
sizeOfSort :: Sort -> Either Blocker SizeOfSort
isSmallSort :: Sort -> Bool
fibrantLub :: IsFibrant -> IsFibrant -> IsFibrant
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

sort :: Sort -> Type Source #

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

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

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 #

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

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

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

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

funSort :: Sort -> Sort -> Sort Source #

univSort :: Sort -> Sort Source #

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

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

lamView :: Term -> ([Arg ArgName], Term) 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.

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 #

argToDontCare :: Arg 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 #

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 #

Everything will be an Abs.

namedTelVars :: Int -> Telescope -> [NamedArg DeBruijnPattern] Source #

telVars :: Int -> Telescope -> [Arg 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 #

levelTm :: Level -> Term Source #

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

fromPatternSubstitution :: PatternSubstitution -> Substitution Source #

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

usePatOrigin :: PatOrigin -> Pattern' a -> Pattern' 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.

type TelView = TelV Type 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.

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.

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

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

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

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

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

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

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

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

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

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

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!

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 #

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

ssort :: Level -> Type Source #

data SizeOfSort Source #

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

Constructors

SmallSort IsFibrant
LargeSort IsFibrant Integer

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 #

fibrantLub :: IsFibrant -> IsFibrant -> IsFibrant Source #

funSort' :: Sort -> Sort -> Either Blocker Sort Source #

Compute the sort of a function type from the sorts of its domain and codomain.

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.

levelMax :: Integer -> [PlusLevel] -> Level 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 #

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

Functor Substitution' Source #

Instance details

Defined in Agda.Syntax.Internal

Methods

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

(<$) :: a -> Substitution' b -> 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 #

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 Int32 Source #

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

value :: Int32 -> 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 #

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 #

Generic (Substitution' a) Source #

Instance details

Defined in Agda.Syntax.Internal

Associated Types

type Rep (Substitution' a)

Instance details

Defined in Agda.Syntax.Internal

type Rep (Substitution' a) = D1 ('MetaData "Substitution'" "Agda.Syntax.Internal" "Agda-2.6.3.1-LLs6QCSf11yD4oGFrJrY5P" 'False) ((C1 ('MetaCons "IdS" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "EmptyS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Impossible)) :+: C1 ('MetaCons ":#" ('InfixI 'RightAssociative 4) 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))))) :+: (C1 ('MetaCons "Strengthen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Impossible) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a)))) :+: (C1 ('MetaCons "Wk" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))) :+: C1 ('MetaCons "Lift" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))))))

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 #

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

Instance details

Defined in Agda.Syntax.Internal

Methods

rnf :: Substitution' a -> () #

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 Rep (Substitution' a) = D1 ('MetaData "Substitution'" "Agda.Syntax.Internal" "Agda-2.6.3.1-LLs6QCSf11yD4oGFrJrY5P" 'False) ((C1 ('MetaCons "IdS" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "EmptyS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Impossible)) :+: C1 ('MetaCons ":#" ('InfixI 'RightAssociative 4) 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))))) :+: (C1 ('MetaCons "Strengthen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Impossible) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a)))) :+: (C1 ('MetaCons "Wk" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))) :+: C1 ('MetaCons "Lift" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Substitution' a))))))

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

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