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

Agda.TypeChecking.Substitute

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

Documentation

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

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

data TelV a Source #

Constructors

TelV 

Fields

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 #

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

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

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

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

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.

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.

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.

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)

projDropParsApply :: Projection -> ProjOrigin -> Relevance -> Args -> Term Source #

projDropParsApply proj o args = projDropPars proj o `apply' args

This function is an optimization, saving us from construction lambdas we immediately remove through application.

telView' :: Type -> TelView Source #

Takes off all exposed function domains from the given type. This means that it does not reduce to expose Pi-types.

telView'UpTo :: Int -> Type -> TelView Source #

telView'UpTo n t takes off the first n exposed function types of t. Takes off all (exposed ones) if n < 0.

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

Add given binding to the front of the telescope.

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

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

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

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

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

Uses free variable analysis to introduce NoAbs bindings.

telePiVisible :: Telescope -> Type -> Type Source #

Only abstract the visible components of the telescope, and all that bind variables. Everything will be an Abs! Caution: quadratic time!

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

typeArgsWithTel :: Telescope -> [Term] -> Maybe [Dom Type] Source #

Given arguments vs : tel (vector typing), extract their individual types. Returns Nothing is tel is not long enough.

compiledClauseBody :: Clause -> Maybe Term Source #

In compiled clauses, the variables in the clause body are relative to the pattern variables (including dot patterns) instead of the clause telescope.

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

univSort' univInf s gets the next higher sort of s, if it is known (i.e. it is not just UnivSort s).

Precondition: s is reduced

data SizeOfSort Source #

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

Constructors

SizeOfSort 

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.

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

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

This function should only be called on reduced sorts, since the LevelUniv rules should only apply when the sort does not reduce to Set.

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

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

piSort' :: Dom Term -> Sort -> Abs Sort -> Either Blocker Sort Source #

Compute the sort of a pi type from the sorts of its domain and codomain. This function should only be called on reduced sorts, since the LevelUniv rules should only apply when the sort doesn't reduce to Set

data Substitution' a Source #

Substitutions.

Constructors

IdS

Identity substitution. Γ ⊢ 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

InstantiateFull Substitution Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

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

Ord Substitution Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

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

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal

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

Defined in Agda.Syntax.Internal.Names

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

Defined in Agda.TypeChecking.Pretty

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

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
Null (Substitution' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

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.4.2-inplace" '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))))))
Show a => Show (Substitution' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

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.4.2-inplace" '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))))))

Orphan instances

Abstract Clause Source # 
Instance details

Abstract Sort Source # 
Instance details

Abstract Telescope Source # 
Instance details

Abstract Term Source # 
Instance details

Abstract Type Source # 
Instance details

Abstract CompiledClauses Source # 
Instance details

Abstract Definition Source # 
Instance details

Abstract Defn Source # 
Instance details

Abstract FunctionInverse Source # 
Instance details

Abstract NumGeneralizableArgs Source # 
Instance details

Abstract PrimFun Source # 
Instance details

Abstract ProjLams Source # 
Instance details

Abstract Projection Source # 
Instance details

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

Abstract System Source # 
Instance details

Abstract Permutation Source # 
Instance details

Apply BraveTerm Source # 
Instance details

Apply Clause Source # 
Instance details

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

Apply Definition Source # 
Instance details

Apply Defn Source # 
Instance details

Methods

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

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

Apply DisplayTerm Source # 
Instance details

Apply ExtLamInfo Source # 
Instance details

Apply FunctionInverse Source # 
Instance details

Apply NumGeneralizableArgs Source # 
Instance details

Apply PrimFun Source # 
Instance details

Apply ProjLams Source # 
Instance details

Apply Projection Source # 
Instance details

Apply RewriteRule Source # 
Instance details

Apply System Source # 
Instance details

Apply Permutation Source # 
Instance details

Subst ProblemEq Source # 
Instance details

Associated Types

type SubstArg ProblemEq 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Name Source # 
Instance details

Associated Types

type SubstArg Name 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst BraveTerm Source # 
Instance details

Associated Types

type SubstArg BraveTerm 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst ConPatternInfo Source # 
Instance details

Associated Types

type SubstArg ConPatternInfo 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst DeBruijnPattern Source # 
Instance details

Associated Types

type SubstArg DeBruijnPattern 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst EqualityTypeData Source # 
Instance details

Associated Types

type SubstArg EqualityTypeData 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst EqualityView Source # 
Instance details

Associated Types

type SubstArg EqualityView 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Pattern Source # 
Instance details

Associated Types

type SubstArg Pattern 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Term Source # 
Instance details

Associated Types

type SubstArg Term 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Range Source # 
Instance details

Associated Types

type SubstArg Range 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Candidate Source # 
Instance details

Associated Types

type SubstArg Candidate 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst CompareAs Source # 
Instance details

Associated Types

type SubstArg CompareAs 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst Constraint Source # 
Instance details

Associated Types

type SubstArg Constraint 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst DisplayForm Source # 
Instance details

Associated Types

type SubstArg DisplayForm 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst DisplayTerm Source # 
Instance details

Associated Types

type SubstArg DisplayTerm 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst LetBinding Source # 
Instance details

Associated Types

type SubstArg LetBinding 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst NLPSort Source # 
Instance details

Associated Types

type SubstArg NLPSort 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst NLPType Source # 
Instance details

Associated Types

type SubstArg NLPType 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst NLPat Source # 
Instance details

Associated Types

type SubstArg NLPat 
Instance details

Defined in Agda.TypeChecking.Substitute

Subst RewriteRule Source # 
Instance details

Associated Types

type SubstArg RewriteRule 
Instance details

Defined in Agda.TypeChecking.Substitute

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

DeBruijn NLPat Source # 
Instance details

Eq Level Source # 
Instance details

Methods

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

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

Eq NotBlocked Source # 
Instance details

Eq PlusLevel Source # 
Instance details

Eq Sort Source # 
Instance details

Methods

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

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

Eq Substitution Source # 
Instance details

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

Eq CandidateKind Source # 
Instance details

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

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

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

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

Abstract [Occurrence] Source # 
Instance details

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

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

Apply [Polarity] Source # 
Instance details

Apply [Occurrence] Source # 
Instance details

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

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

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
Subst a => Subst (PlusLevel' a) Source # 
Instance details

Associated Types

type SubstArg (PlusLevel' a) 
Instance details

Defined in Agda.TypeChecking.Substitute

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

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