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

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

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

(Subst Term a, Eq a) => Eq (TelV a)

Defined in Agda.TypeChecking.Substitute

Methods

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

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

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

Show a => Show (TelV a)

Defined in Agda.TypeChecking.Substitute

Methods

showsPrec :: Int -> TelV a -> ShowS

show :: TelV a -> String

showList :: [TelV a] -> ShowS

type TelView = TelV Type

applyTermE :: forall t. (Coercible Term t, Apply t, Subst t 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.

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

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

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

Eliminate a constructed term.

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.

argToDontCare :: Arg Term -> Term

relToDontCare :: LensRelevance a => a -> 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.

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

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

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

renaming :: forall a. DeBruijn a => Empty -> Permutation -> Substitution' a

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

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

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

renameP :: Subst t a => Empty -> Permutation -> a -> a

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

applySubstTerm :: forall t. (Coercible t Term, Subst t t, Apply t) => Substitution' t -> t -> t

applyNLPatSubst :: Subst Term a => Substitution' NLPat -> a -> a

applyNLSubstToDom :: Subst NLPat a => Substitution' NLPat -> Dom a -> Dom a

fromPatternSubstitution :: PatternSubstitution -> Substitution

applyPatSubst :: Subst Term 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.

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.

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

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

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

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

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

domFromNamedArgName :: NamedArg Name -> Dom ()

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

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

mkLam :: Arg ArgName -> Term -> Term

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

telePi :: Telescope -> Type -> Type

Uses free variable analysis to introduce NoAbs bindings.

telePi_ :: Telescope -> Type -> Type

Everything will be an Abs.

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!

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.

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' :: Maybe Sort -> Sort -> Maybe Sort

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

Precondition: s is reduced

univSort :: Maybe Sort -> Sort -> Sort

univInf :: HasOptions m => m (Maybe Sort)

funSort' :: Sort -> Sort -> Maybe Sort

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

funSort :: Sort -> Sort -> Sort

piSort' :: Dom Type -> Abs Sort -> Maybe Sort

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

piSort :: Dom Type -> Abs Sort -> Sort

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

levelLub :: Level -> Level -> Level

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

levelTm :: Level -> Term

unLevelAtom :: LevelAtom -> Term

module Agda.TypeChecking.Substitute.Class

module Agda.TypeChecking.Substitute.DeBruijn

data Substitution' a

Substitutions.

Constructors

IdS

Identity substitution. Γ ⊢ IdS : Γ

EmptyS Empty

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 Empty (Substitution' a)

Strengthening substitution. First argument is IMPOSSIBLE. Apply this to a term which does not contain variable 0 to lower all de Bruijn indices by one. Γ ⊢ ρ : Δ --------------------------- Γ ⊢ Strengthen ρ : Δ, A

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

Eq Substitution

Defined in Agda.TypeChecking.Substitute

Methods

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

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

Functor Substitution'

Defined in Agda.Syntax.Internal

Methods

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

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

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

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)

KillRange Substitution

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT Substitution

InstantiateFull Substitution

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: Substitution -> ReduceM Substitution

Subst a a => Subst a (Substitution' a)

Defined in Agda.TypeChecking.Substitute

Methods

applySubst :: Substitution' a -> Substitution' a -> Substitution' a

Data a => Data (Substitution' a)

Defined in Agda.Syntax.Internal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Substitution' a -> c (Substitution' a)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Substitution' a)

toConstr :: Substitution' a -> Constr

dataTypeOf :: Substitution' a -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Substitution' a))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Substitution' a))

gmapT :: (forall b. Data b => b -> b) -> Substitution' a -> Substitution' a

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Substitution' a -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Substitution' a -> r

gmapQ :: (forall d. Data d => d -> u) -> Substitution' a -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Substitution' a -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Substitution' a -> m (Substitution' a)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Substitution' a -> m (Substitution' a)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Substitution' a -> m (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

Null (Substitution' a)

Defined in Agda.Syntax.Internal

Methods

empty :: Substitution' a

null :: Substitution' a -> Bool

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

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)

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

Defined in Agda.TypeChecking.Pretty

Methods

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

type Substitution = Substitution' Term

Orphan instances

Eq Substitution

Methods

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

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

Eq NotBlocked

Methods

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

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

Eq LevelAtom

Methods

(==) :: LevelAtom -> LevelAtom -> Bool

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

Eq PlusLevel

Methods

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

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

Eq Level

Methods

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

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

Eq Sort

Methods

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

(/=) :: Sort -> Sort -> 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 Section

Methods

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

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

Eq CompareAs

Methods

(==) :: CompareAs -> CompareAs -> Bool

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

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 LevelAtom

Methods

compare :: LevelAtom -> LevelAtom -> Ordering

(<) :: LevelAtom -> LevelAtom -> Bool

(<=) :: LevelAtom -> LevelAtom -> Bool

(>) :: LevelAtom -> LevelAtom -> Bool

(>=) :: LevelAtom -> LevelAtom -> Bool

max :: LevelAtom -> LevelAtom -> LevelAtom

min :: LevelAtom -> LevelAtom -> LevelAtom

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

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

Abstract Permutation

Methods

abstract :: Telescope -> Permutation -> Permutation

Abstract Clause

Methods

abstract :: Telescope -> Clause -> Clause

Abstract Sort

Methods

abstract :: Telescope -> Sort -> Sort

Abstract Telescope

Methods

abstract :: Telescope -> Telescope -> Telescope

Abstract Type

Methods

abstract :: Telescope -> Type -> Type

Abstract Term

Methods

abstract :: Telescope -> Term -> Term

Abstract CompiledClauses

Methods

abstract :: Telescope -> CompiledClauses -> CompiledClauses

Abstract FunctionInverse

Methods

abstract :: Telescope -> FunctionInverse -> FunctionInverse

Abstract PrimFun

Methods

abstract :: Telescope -> PrimFun -> PrimFun

Abstract Defn

Methods

abstract :: Telescope -> Defn -> Defn

Abstract ProjLams

Methods

abstract :: Telescope -> ProjLams -> ProjLams

Abstract Projection

Methods

abstract :: Telescope -> Projection -> Projection

Abstract System

Methods

abstract :: Telescope -> System -> System

Abstract NumGeneralizableArgs

Methods

abstract :: Telescope -> NumGeneralizableArgs -> NumGeneralizableArgs

Abstract Definition

Methods

abstract :: Telescope -> Definition -> Definition

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

Apply Permutation

Methods

apply :: Permutation -> Args -> Permutation

applyE :: Permutation -> Elims -> Permutation

Apply Clause

Methods

apply :: Clause -> Args -> Clause

applyE :: Clause -> Elims -> Clause

Apply BraveTerm

Methods

apply :: BraveTerm -> Args -> BraveTerm

applyE :: BraveTerm -> Elims -> BraveTerm

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 FunctionInverse

Methods

apply :: FunctionInverse -> Args -> FunctionInverse

applyE :: FunctionInverse -> Elims -> FunctionInverse

Apply PrimFun

Methods

apply :: PrimFun -> Args -> PrimFun

applyE :: PrimFun -> Elims -> PrimFun

Apply Defn

Methods

apply :: Defn -> Args -> Defn

applyE :: Defn -> Elims -> Defn

Apply ProjLams

Methods

apply :: ProjLams -> Args -> ProjLams

applyE :: ProjLams -> Elims -> ProjLams

Apply Projection

Methods

apply :: Projection -> Args -> Projection

applyE :: Projection -> Elims -> Projection

Apply ExtLamInfo

Methods

apply :: ExtLamInfo -> Args -> ExtLamInfo

applyE :: ExtLamInfo -> Elims -> ExtLamInfo

Apply System

Methods

apply :: System -> Args -> System

applyE :: System -> Elims -> System

Apply NumGeneralizableArgs

Methods

apply :: NumGeneralizableArgs -> Args -> NumGeneralizableArgs

applyE :: NumGeneralizableArgs -> Elims -> NumGeneralizableArgs

Apply Definition

Methods

apply :: Definition -> Args -> Definition

applyE :: Definition -> Elims -> Definition

Apply RewriteRule

Methods

apply :: RewriteRule -> Args -> RewriteRule

applyE :: RewriteRule -> Elims -> RewriteRule

Apply DisplayTerm

Methods

apply :: DisplayTerm -> Args -> DisplayTerm

applyE :: DisplayTerm -> Elims -> DisplayTerm

Subst DeBruijnPattern DeBruijnPattern

Methods

applySubst :: Substitution' DeBruijnPattern -> DeBruijnPattern -> DeBruijnPattern

Subst BraveTerm BraveTerm

Methods

applySubst :: Substitution' BraveTerm -> BraveTerm -> BraveTerm

Subst Term ()

Methods

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

Subst Term String

Methods

applySubst :: Substitution' Term -> String -> String

Subst Term Range

Methods

applySubst :: Substitution' Term -> Range -> Range

Subst Term Name

Methods

applySubst :: Substitution' Term -> Name -> Name

Subst Term EqualityView

Methods

applySubst :: Substitution' Term -> EqualityView -> EqualityView

Subst Term ConPatternInfo

Methods

applySubst :: Substitution' Term -> ConPatternInfo -> ConPatternInfo

Subst Term Pattern

Methods

applySubst :: Substitution' Term -> Pattern -> Pattern

Subst Term Term

Methods

applySubst :: Substitution' Term -> Term -> Term

Subst Term ProblemEq

Methods

applySubst :: Substitution' Term -> ProblemEq -> ProblemEq

Subst Term Candidate

Methods

applySubst :: Substitution' Term -> Candidate -> Candidate

Subst Term DisplayTerm

Methods

applySubst :: Substitution' Term -> DisplayTerm -> DisplayTerm

Subst Term DisplayForm

Methods

applySubst :: Substitution' Term -> DisplayForm -> DisplayForm

Subst Term CompareAs

Methods

applySubst :: Substitution' Term -> CompareAs -> CompareAs

Subst Term Constraint

Methods

applySubst :: Substitution' Term -> Constraint -> Constraint

Subst NLPat RewriteRule

Methods

applySubst :: Substitution' NLPat -> RewriteRule -> RewriteRule

Subst NLPat NLPSort

Methods

applySubst :: Substitution' NLPat -> NLPSort -> NLPSort

Subst NLPat NLPType

Methods

applySubst :: Substitution' NLPat -> NLPType -> NLPType

Subst NLPat NLPat

Methods

applySubst :: Substitution' NLPat -> NLPat -> NLPat

Subst t a => Subst t (WithHiding a)

Methods

applySubst :: Substitution' t -> WithHiding a -> WithHiding a

Subst t a => Subst t [a]

Methods

applySubst :: Substitution' t -> [a] -> [a]

Subst t a => Subst t (Maybe a)

Methods

applySubst :: Substitution' t -> Maybe a -> Maybe a

Subst t a => Subst t (Arg a)

Methods

applySubst :: Substitution' t -> Arg a -> Arg a

Subst t a => Subst t (Abs a)

Methods

applySubst :: Substitution' t -> Abs a -> Abs a

Subst t a => Subst t (Elim' a)

Methods

applySubst :: Substitution' t -> Elim' a -> Elim' a

Subst t a => Subst t (Tele a)

Methods

applySubst :: Substitution' t -> Tele a -> Tele a

Subst t a => Subst t (Blocked a)

Methods

applySubst :: Substitution' t -> Blocked a -> Blocked a

Subst t a => Subst t (LevelAtom' a)

Methods

applySubst :: Substitution' t -> LevelAtom' a -> LevelAtom' a

Subst t a => Subst t (PlusLevel' a)

Methods

applySubst :: Substitution' t -> PlusLevel' a -> PlusLevel' a

Subst t a => Subst t (Level' a)

Methods

applySubst :: Substitution' t -> Level' a -> Level' a

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

Methods

applySubst :: Substitution' t -> Sort' a -> Sort' a

Subst a a => Subst a (Substitution' a)

Methods

applySubst :: Substitution' a -> Substitution' a -> Substitution' a

(Subst t a, Subst t b) => Subst t (a, b)

Methods

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

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

Methods

applySubst :: Substitution' t -> Map k a -> Map k a

(Subst t a, Subst t b) => Subst t (Dom' a b)

Methods

applySubst :: Substitution' t -> Dom' a b -> Dom' a b

Subst t a => Subst t (Named name a)

Methods

applySubst :: Substitution' t -> Named name a -> Named name a

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

Methods

applySubst :: Substitution' t -> Type'' a b -> Type'' a b

(Subst t a, Subst t b, Subst t c) => Subst t (a, b, c)

Methods

applySubst :: Substitution' t -> (a, b, c) -> (a, b, c)

(Subst t a, Subst t b, Subst t c, Subst t d) => Subst t (a, b, c, d)

Methods

applySubst :: Substitution' t -> (a, b, c, d) -> (a, b, c, d)

Eq a => Eq (Pattern' a)

Methods

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

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

Eq t => Eq (Blocked t)

Methods

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

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

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

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

Methods

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

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

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

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

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

DeBruijn a => DeBruijn (Pattern' a)

Methods

deBruijnVar :: Int -> Pattern' a

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

deBruijnView :: Pattern' a -> Maybe Int

Abstract t => Abstract [t]

Methods

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

Abstract [Polarity]

Methods

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

Abstract [Occurrence]

Methods

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

Abstract t => Abstract (Maybe t)

Methods

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

DoDrop a => Abstract (Drop a)

Methods

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

Abstract a => Abstract (Case a)

Methods

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

Abstract a => Abstract (WithArity a)

Methods

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

Apply t => Apply [t]

Methods

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

applyE :: [t] -> Elims -> [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 (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

DoDrop a => Apply (Drop a)

Methods

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

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

Apply t => Apply (Blocked t)

Methods

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

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

Subst Term 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

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 a, Apply b) => Apply (a, b)

Methods

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

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

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 c) => Apply (a, b, c)

Methods

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

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