Agda.TypeChecking.Substitute

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.

Documentation

sort :: Sort -> Type

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

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

data TelV a

Constructors

TelV

Fields

• theTel :: Tele (Dom a)
• theCore :: a

Instances

Functor TelV

Defined in Agda.TypeChecking.Substitute

Methods

fmap :: (a -> b) -> TelV a -> TelV b

(<$) :: a -> TelV b -> TelV a

Show a => Show (TelV a)

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)

Defined in Agda.TypeChecking.Substitute

Methods

(==) :: TelV a -> TelV a -> Bool

(/=) :: TelV a -> TelV a -> Bool

(TermSubst a, Ord a) => Ord (TelV a)

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

funSort :: Sort -> Sort -> Sort

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

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

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

univSort :: Sort -> Sort

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

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

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

applyTermE :: (Coercible Term t, Apply t, EndoSubst t) => (Empty -> Term -> Elims -> Term) -> t -> Elims -> t

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

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

Eliminate a constructed term.

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

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

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

argToDontCare :: Arg Term -> Term

piApply :: Type -> Args -> Type

(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

teleLam :: Telescope -> Term -> Term

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

Everything will be an Abs.

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

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

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

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

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

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

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

telView' :: Type -> TelView

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

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

Add given binding to the front of the telescope.

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

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

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

Turn a typed binding (x1 .. xn : A) into a 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

Uses free variable analysis to introduce NoAbs bindings.

telePiVisible :: Telescope -> Type -> Type

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

Performs void (noAbs) abstraction over telescope.

Methods

teleNoAbs :: a -> Term -> Term

Instances

TeleNoAbs ListTel

Defined in Agda.TypeChecking.Substitute

Methods

teleNoAbs :: ListTel -> Term -> Term

TeleNoAbs Telescope

Defined in Agda.TypeChecking.Substitute

Methods

teleNoAbs :: Telescope -> Term -> Term

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

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

compiledClauseBody :: Clause -> Maybe Term

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

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

data SizeOfSort

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

Constructors

SizeOfSort

Fields

• szSortUniv :: Univ
• szSortSize :: Integer

pattern SmallSort :: Univ -> SizeOfSort

pattern LargeSort :: Univ -> Integer -> SizeOfSort

sizeOfSort :: Sort -> Either Blocker SizeOfSort

Returns Left blocker for unknown (blocked) sorts, and otherwise returns Right s where s indicates the size and fibrancy.

isSmallSort :: Sort -> Bool

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

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

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

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

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

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

module Agda.TypeChecking.Substitute.Class

module Agda.TypeChecking.Substitute.DeBruijn

data Substitution' a

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

KillRange Substitution

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Substitution

InstantiateFull Substitution

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Substitution -> ReduceM Substitution

Foldable Substitution'

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'

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'

Defined in Agda.Syntax.Internal

Methods

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

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

Eq Substitution

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Ord Substitution

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)

Defined in Agda.Syntax.Internal

Methods

pretty :: Substitution' a -> Doc

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

prettyList :: [Substitution' a] -> Doc

TermSize a => TermSize (Substitution' a)

Defined in Agda.Syntax.Internal

Methods

termSize :: Substitution' a -> Int

tsize :: Substitution' a -> Sum Int

NamesIn a => NamesIn (Substitution' a)

Defined in Agda.Syntax.Internal.Names

Methods

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

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

Defined in Agda.TypeChecking.Pretty

Methods

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

EmbPrj a => EmbPrj (Substitution' a)

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Substitution' a -> S Int32

icod_ :: Substitution' a -> S Int32

value :: Int32 -> R (Substitution' a)

EndoSubst a => Subst (Substitution' a)

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Substitution' a)

Defined in Agda.TypeChecking.Substitute

type SubstArg (Substitution' a) = a

Methods

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

Null (Substitution' a)

Defined in Agda.Syntax.Internal

Methods

empty :: Substitution' a

null :: Substitution' a -> Bool

Generic (Substitution' a)

Defined in Agda.Syntax.Internal

Associated Types

type Rep (Substitution' a)

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

Methods

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

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

Show a => Show (Substitution' a)

Defined in Agda.Syntax.Internal

Methods

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

show :: Substitution' a -> String

showList :: [Substitution' a] -> ShowS

NFData a => NFData (Substitution' a)

Defined in Agda.Syntax.Internal

Methods

rnf :: Substitution' a -> ()

type SubstArg (Substitution' a)

Defined in Agda.TypeChecking.Substitute

type SubstArg (Substitution' a) = a

type Rep (Substitution' a)

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

type Substitution = Substitution' Term

Orphan instances

Abstract Clause

Methods

abstract :: Telescope -> Clause -> Clause

Abstract Sort

Methods

abstract :: Telescope -> Sort -> Sort

Abstract Telescope

Methods

abstract :: Telescope -> Telescope -> Telescope

Abstract Term

Methods

abstract :: Telescope -> Term -> Term

Abstract Type

Methods

abstract :: Telescope -> Type -> Type

Abstract CompiledClauses

Methods

abstract :: Telescope -> CompiledClauses -> CompiledClauses

Abstract Definition

Methods

abstract :: Telescope -> Definition -> Definition

Abstract Defn

Methods

abstract :: Telescope -> Defn -> Defn

Abstract FunctionInverse

Methods

abstract :: Telescope -> FunctionInverse -> FunctionInverse

Abstract NumGeneralizableArgs

Methods

abstract :: Telescope -> NumGeneralizableArgs -> NumGeneralizableArgs

Abstract PrimFun

Methods

abstract :: Telescope -> PrimFun -> PrimFun

Abstract ProjLams

Methods

abstract :: Telescope -> ProjLams -> ProjLams

Abstract Projection

Methods

abstract :: Telescope -> Projection -> Projection

Abstract RewriteRule

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'.

Methods

abstract :: Telescope -> RewriteRule -> RewriteRule

Abstract System

Methods

abstract :: Telescope -> System -> System

Abstract Permutation

Methods

abstract :: Telescope -> Permutation -> Permutation

Apply BraveTerm

Methods

apply :: BraveTerm -> Args -> BraveTerm

applyE :: BraveTerm -> Elims -> BraveTerm

Apply Clause

Methods

apply :: Clause -> Args -> Clause

applyE :: Clause -> Elims -> Clause

Apply Sort

Methods

apply :: Sort -> Args -> Sort

applyE :: Sort -> Elims -> Sort

Apply Term

Methods

apply :: Term -> Args -> Term

applyE :: Term -> Elims -> Term

Apply CompiledClauses

Methods

apply :: CompiledClauses -> Args -> CompiledClauses

applyE :: CompiledClauses -> Elims -> CompiledClauses

Apply Definition

Methods

apply :: Definition -> Args -> Definition

applyE :: Definition -> Elims -> Definition

Apply Defn

Methods

apply :: Defn -> Args -> Defn

applyE :: Defn -> Elims -> Defn

Apply DisplayTerm

Methods

apply :: DisplayTerm -> Args -> DisplayTerm

applyE :: DisplayTerm -> Elims -> DisplayTerm

Apply ExtLamInfo

Methods

apply :: ExtLamInfo -> Args -> ExtLamInfo

applyE :: ExtLamInfo -> Elims -> ExtLamInfo

Apply FunctionInverse

Methods

apply :: FunctionInverse -> Args -> FunctionInverse

applyE :: FunctionInverse -> Elims -> FunctionInverse

Apply NumGeneralizableArgs

Methods

apply :: NumGeneralizableArgs -> Args -> NumGeneralizableArgs

applyE :: NumGeneralizableArgs -> Elims -> NumGeneralizableArgs

Apply PrimFun

Methods

apply :: PrimFun -> Args -> PrimFun

applyE :: PrimFun -> Elims -> PrimFun

Apply ProjLams

Methods

apply :: ProjLams -> Args -> ProjLams

applyE :: ProjLams -> Elims -> ProjLams

Apply Projection

Methods

apply :: Projection -> Args -> Projection

applyE :: Projection -> Elims -> Projection

Apply RewriteRule

Methods

apply :: RewriteRule -> Args -> RewriteRule

applyE :: RewriteRule -> Elims -> RewriteRule

Apply System

Methods

apply :: System -> Args -> System

applyE :: System -> Elims -> System

Apply Permutation

Methods

apply :: Permutation -> Args -> Permutation

applyE :: Permutation -> Elims -> Permutation

Subst ProblemEq

Associated Types

type SubstArg ProblemEq

Defined in Agda.TypeChecking.Substitute

type SubstArg ProblemEq = Term

Methods

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

Subst Name

Associated Types

type SubstArg Name

Defined in Agda.TypeChecking.Substitute

type SubstArg Name = Term

Methods

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

Subst BraveTerm

Associated Types

type SubstArg BraveTerm

Defined in Agda.TypeChecking.Substitute

type SubstArg BraveTerm = BraveTerm

Methods

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

Subst ConPatternInfo

Associated Types

type SubstArg ConPatternInfo

Defined in Agda.TypeChecking.Substitute

type SubstArg ConPatternInfo = Term

Methods

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

Subst DeBruijnPattern

Associated Types

type SubstArg DeBruijnPattern

Defined in Agda.TypeChecking.Substitute

type SubstArg DeBruijnPattern = DeBruijnPattern

Methods

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

Subst EqualityTypeData

Associated Types

type SubstArg EqualityTypeData

Defined in Agda.TypeChecking.Substitute

type SubstArg EqualityTypeData = Term

Methods

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

Subst EqualityView

Associated Types

type SubstArg EqualityView

Defined in Agda.TypeChecking.Substitute

type SubstArg EqualityView = Term

Methods

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

Subst Pattern

Associated Types

type SubstArg Pattern

Defined in Agda.TypeChecking.Substitute

type SubstArg Pattern = Term

Methods

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

Subst Term

Associated Types

type SubstArg Term

Defined in Agda.TypeChecking.Substitute

type SubstArg Term = Term

Methods

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

Subst Range

Associated Types

type SubstArg Range

Defined in Agda.TypeChecking.Substitute

type SubstArg Range = Term

Methods

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

Subst Candidate

Associated Types

type SubstArg Candidate

Defined in Agda.TypeChecking.Substitute

type SubstArg Candidate = Term

Methods

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

Subst CompareAs

Associated Types

type SubstArg CompareAs

Defined in Agda.TypeChecking.Substitute

type SubstArg CompareAs = Term

Methods

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

Subst Constraint

Associated Types

type SubstArg Constraint

Defined in Agda.TypeChecking.Substitute

type SubstArg Constraint = Term

Methods

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

Subst DisplayForm

Associated Types

type SubstArg DisplayForm

Defined in Agda.TypeChecking.Substitute

type SubstArg DisplayForm = Term

Methods

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

Subst DisplayTerm

Associated Types

type SubstArg DisplayTerm

Defined in Agda.TypeChecking.Substitute

type SubstArg DisplayTerm = Term

Methods

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

Subst LetBinding

Associated Types

type SubstArg LetBinding

Defined in Agda.TypeChecking.Substitute

type SubstArg LetBinding = Term

Methods

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

Subst NLPSort

Associated Types

type SubstArg NLPSort

Defined in Agda.TypeChecking.Substitute

type SubstArg NLPSort = NLPat

Methods

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

Subst NLPType

Associated Types

type SubstArg NLPType

Defined in Agda.TypeChecking.Substitute

type SubstArg NLPType = NLPat

Methods

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

Subst NLPat

Associated Types

type SubstArg NLPat

Defined in Agda.TypeChecking.Substitute

type SubstArg NLPat = NLPat

Methods

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

Subst RewriteRule

Associated Types

type SubstArg RewriteRule

Defined in Agda.TypeChecking.Substitute

type SubstArg RewriteRule = NLPat

Methods

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

Subst ()

Associated Types

type SubstArg ()

Defined in Agda.TypeChecking.Substitute

type SubstArg () = Term

Methods

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

DeBruijn BraveTerm

Methods

deBruijnVar :: Int -> BraveTerm

debruijnNamedVar :: String -> Int -> BraveTerm

deBruijnView :: BraveTerm -> Maybe Int

DeBruijn NLPat

Methods

deBruijnVar :: Int -> NLPat

debruijnNamedVar :: String -> Int -> NLPat

deBruijnView :: NLPat -> Maybe Int

Eq Level

Methods

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

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

Eq NotBlocked

Methods

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

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

Eq PlusLevel

Methods

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

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

Eq Sort

Methods

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

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

Eq Substitution

Methods

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

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

Eq Term

Syntactic Term equality, ignores stuff below DontCare and sharing.

Methods

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

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

Eq Candidate

Methods

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

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

Eq CandidateKind

Methods

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

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

Eq Section

Methods

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

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

Ord Level

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

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

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

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

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)

Methods

abstract :: Telescope -> Case a -> Case a

Abstract a => Abstract (WithArity a)

Methods

abstract :: Telescope -> WithArity a -> WithArity a

DoDrop a => Abstract (Drop a)

Methods

abstract :: Telescope -> Drop a -> Drop a

Abstract t => Abstract (Maybe t)

Methods

abstract :: Telescope -> Maybe t -> Maybe t

Abstract [Polarity]

Methods

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

Abstract [Occurrence]

Methods

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

Abstract t => Abstract [t]

Methods

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

Apply t => Apply (Blocked t)

Methods

apply :: Blocked t -> Args -> Blocked t

applyE :: Blocked t -> Elims -> Blocked t

TermSubst a => Apply (Tele a)

Methods

apply :: Tele a -> Args -> Tele a

applyE :: Tele a -> Elims -> Tele a

Apply a => Apply (Case a)

Methods

apply :: Case a -> Args -> Case a

applyE :: Case a -> Elims -> Case a

Apply a => Apply (WithArity a)

Methods

apply :: WithArity a -> Args -> WithArity a

applyE :: WithArity a -> Elims -> WithArity a

DoDrop a => Apply (Drop a)

Methods

apply :: Drop a -> Args -> Drop a

applyE :: Drop a -> Elims -> Drop a

Apply t => Apply (Maybe t)

Methods

apply :: Maybe t -> Args -> Maybe t

applyE :: Maybe t -> Elims -> Maybe t

Apply t => Apply (Maybe t)

Methods

apply :: Maybe t -> Args -> Maybe t

applyE :: Maybe t -> Elims -> Maybe t

Apply [NamedArg (Pattern' a)]

Make sure we only drop variable patterns.

Methods

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

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

Apply [Polarity]

Methods

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

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

Apply [Occurrence]

Methods

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

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

Apply t => Apply [t]

Methods

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

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

Subst a => Subst (Arg a)

Associated Types

type SubstArg (Arg a)

Defined in Agda.TypeChecking.Substitute

type SubstArg (Arg a) = SubstArg a

Methods

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

Subst a => Subst (WithHiding a)

Associated Types

type SubstArg (WithHiding a)

Defined in Agda.TypeChecking.Substitute

type SubstArg (WithHiding a) = SubstArg a

Methods

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

Subst a => Subst (Abs a)

Associated Types

type SubstArg (Abs a)

Defined in Agda.TypeChecking.Substitute

type SubstArg (Abs a) = SubstArg a

Methods

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

Subst a => Subst (Blocked a)

Associated Types

type SubstArg (Blocked a)

Defined in Agda.TypeChecking.Substitute

type SubstArg (Blocked a) = SubstArg a

Methods

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

Subst a => Subst (Level' a)

Associated Types

type SubstArg (Level' a)

Defined in Agda.TypeChecking.Substitute

type SubstArg (Level' a) = SubstArg a

Methods

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

Subst a => Subst (PlusLevel' a)

Associated Types

type SubstArg (PlusLevel' a)

Defined in Agda.TypeChecking.Substitute

type SubstArg (PlusLevel' a) = SubstArg a

Methods

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

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

Associated Types

type SubstArg (Sort' a)

Defined in Agda.TypeChecking.Substitute

type SubstArg (Sort' a) = SubstArg a

Methods

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

EndoSubst a => Subst (Substitution' a)

Associated Types

type SubstArg (Substitution' a)

Defined in Agda.TypeChecking.Substitute

type SubstArg (Substitution' a) = a

Methods

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

Subst a => Subst (Tele a)

Associated Types

type SubstArg (Tele a)

Defined in Agda.TypeChecking.Substitute

type SubstArg (Tele a) = SubstArg a

Methods

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

Subst a => Subst (Elim' a)

Associated Types

type SubstArg (Elim' a)

Defined in Agda.TypeChecking.Substitute

type SubstArg (Elim' a) = SubstArg a

Methods

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

Subst a => Subst (Maybe a)

Associated Types

type SubstArg (Maybe a)

Defined in Agda.TypeChecking.Substitute

type SubstArg (Maybe a) = SubstArg a

Methods

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

Subst a => Subst [a]

Associated Types

type SubstArg [a]

Defined in Agda.TypeChecking.Substitute

type SubstArg [a] = SubstArg a

Methods

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

DeBruijn a => DeBruijn (Pattern' a)

Methods

deBruijnVar :: Int -> Pattern' a

debruijnNamedVar :: String -> Int -> Pattern' a

deBruijnView :: Pattern' a -> Maybe Int

(Subst a, Eq a) => Eq (Abs a)

Equality of binders relies on weakening which is a special case of renaming which is a special case of substitution.

Methods

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

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

Eq t => Eq (Blocked t)

Methods

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

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

Eq a => Eq (Pattern' a)

Methods

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

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

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

Methods

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

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

Eq a => Eq (Type' a)

Syntactic Type equality, ignores sort annotations.

Methods

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

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

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

Methods

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

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

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

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)

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)

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)

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)

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)

Methods

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

Abstract v => Abstract (HashMap k v)

Methods

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

Apply v => Apply (Map k v)

Methods

apply :: Map k v -> Args -> Map k v

applyE :: Map k v -> Elims -> Map k v

Apply v => Apply (HashMap k v)

Methods

apply :: HashMap k v -> Args -> HashMap k v

applyE :: HashMap k v -> Elims -> HashMap k v

(Apply a, Apply b) => Apply (a, b)

Methods

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

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

Subst a => Subst (Named name a)

Associated Types

type SubstArg (Named name a)

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

(Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (Dom' a b)

Associated Types

type SubstArg (Dom' a b)

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

(Coercible a Term, Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (Type'' a b)

Associated Types

type SubstArg (Type'' a b)

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

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

Associated Types

type SubstArg (Map k a)

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

(Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (a, b)

Associated Types

type SubstArg (a, b)

Defined in Agda.TypeChecking.Substitute

type SubstArg (a, b) = SubstArg a

Methods

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

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

Methods

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

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

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

Associated Types

type SubstArg (a, b, c)

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)

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

Associated Types

type SubstArg (a, b, c, d)

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)