Agda.TypeChecking.Substitute

Documentation

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

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

conApp :: ConHead -> ConInfo -> Args -> 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

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.

Abstraction

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

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

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

Substitution and raisingshiftingweakening

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)

fromPatternSubstitution :: PatternSubstitution -> Substitution

applyPatSubst :: Subst Term a => PatternSubstitution -> a -> a

Projections

projDropParsApply :: Projection -> ProjOrigin -> 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.

Telescopes

type TelView = TelV Type

data TelV a

Constructors

TelV

Fields

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

Instances

Functor TelV

Methods

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

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

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

Methods

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

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

(Subst t a, Ord a) => Ord (TelV a)

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)

Methods

showsPrec :: Int -> TelV a -> ShowS

show :: TelV a -> String

showList :: [TelV a] -> ShowS

type ListTel' a = [Dom (a, Type)]

type ListTel = ListTel' ArgName

telFromList' :: (a -> ArgName) -> ListTel' a -> Telescope

telFromList :: ListTel -> Telescope

telToList :: Telescope -> ListTel

telToArgs :: Telescope -> [Arg ArgName]

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

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

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

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

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

bindsWithHidingToTel :: [WithHiding Name] -> Dom Type -> ListTel

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.

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 a Abs.

teleLam :: Telescope -> Term -> Term

class TeleNoAbs a where

Performs void (noAbs) abstraction over telescope.

Minimal complete definition

teleNoAbs

Methods

teleNoAbs :: a -> Term -> Term

Instances

TeleNoAbs Telescope

Methods

teleNoAbs :: Telescope -> Term -> Term

TeleNoAbs ListTel

Methods

teleNoAbs :: ListTel -> Term -> Term

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.

Syntactic equality and order

Level stuff

pts :: Sort -> Sort -> Sort

The `rule', if Agda is considered as a functional pure type system (pts).

TODO: This needs to be properly implemented, requiring refactoring of Agda's handling of levels. Without impredicativity or SizeUniv, Agda's pts rule is just the least upper bound, which is total and commutative. The handling of levels relies on this simplification.

sLub :: Sort -> Sort -> Sort

dLub :: Sort -> Abs Sort -> Sort

Dependent least upper bound, to assign a level to expressions like forall i -> Set i.

dLub s1 i.s2 = omega if i appears in the rigid variables of s2.

lvlView :: Term -> Level

levelMax :: [PlusLevel] -> Level

sortTm :: Sort -> Term

levelSort :: Level -> Sort

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 substitution, lifts from the empty context. 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)

Weakning 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

Functor Substitution'

Methods

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

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

Foldable Substitution'

Methods

fold :: Monoid m => Substitution' m -> 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'

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

Methods

killRange :: KillRangeT Substitution

InstantiateFull Substitution

Methods

instantiateFull' :: Substitution -> ReduceM Substitution

Show a => Show (Substitution' a)

Methods

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

show :: Substitution' a -> String

showList :: [Substitution' a] -> ShowS

Pretty a => Pretty (Substitution' a)

Methods

pretty :: Substitution' a -> Doc

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

Null (Substitution' a)

Methods

empty :: Substitution' a

null :: Substitution' a -> Bool

TermSize a => TermSize (Substitution' a)

Methods

termSize :: Substitution' a -> Int

tsize :: Substitution' a -> Sum Int

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

Methods

prettyTCM :: Substitution' a -> TCM Doc

type Substitution = Substitution' Term

Orphan instances

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 Constraint

Methods

(==) :: Constraint -> Constraint -> Bool

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

Ord NotBlocked

Methods

compare :: NotBlocked -> NotBlocked -> Ordering

(<) :: NotBlocked -> NotBlocked -> Bool

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

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

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

max :: NotBlocked -> NotBlocked -> NotBlocked

min :: NotBlocked -> NotBlocked -> NotBlocked

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 DeBruijnPattern

Methods

deBruijnVar :: Int -> DeBruijnPattern

debruijnNamedVar :: String -> Int -> DeBruijnPattern

deBruijnView :: DeBruijnPattern -> 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 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 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 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 Term ()

Methods

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

Subst Term String

Methods

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

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 LevelAtom

Methods

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

Subst Term PlusLevel

Methods

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

Subst Term Level

Methods

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

Subst Term Sort

Methods

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

Subst Term Term

Methods

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

Subst Term NamedDotPattern

Methods

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

Subst Term Candidate

Methods

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

Subst Term ModuleParameters

Methods

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

Subst Term RewriteRule

Methods

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

Subst Term NLPType

Methods

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

Subst Term NLPat

Methods

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

Subst Term DisplayTerm

Methods

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

Subst Term DisplayForm

Methods

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

Subst Term Constraint

Methods

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

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

Methods

applySubst :: Substitution' t -> Dom a -> Dom 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 (Ptr a)

Methods

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

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

Methods

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

Subst Term a => Subst Term (Type' a)

Methods

applySubst :: Substitution' Term -> Type' a -> Type' 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 (Named name a)

Methods

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

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

Methods

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

(/=) :: Substitution' Term -> Substitution' Term -> 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)

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

Ord (Substitution' Term)

Methods

compare :: Substitution' Term -> Substitution' Term -> Ordering

(<) :: Substitution' Term -> Substitution' Term -> Bool

(<=) :: Substitution' Term -> Substitution' Term -> Bool

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

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

max :: Substitution' Term -> Substitution' Term -> Substitution' Term

min :: Substitution' Term -> Substitution' Term -> Substitution' Term

Ord t => Ord (Blocked t)

Methods

compare :: Blocked t -> Blocked t -> Ordering

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

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

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

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

max :: Blocked t -> Blocked t -> Blocked t

min :: Blocked t -> Blocked t -> Blocked t

(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

Abstract t => Abstract [t]

Methods

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

Abstract [Occurrence]

Methods

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

Abstract [Polarity]

Methods

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

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 [Occurrence]

Methods

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

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

Apply [Polarity]

Methods

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

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

Apply t => Apply (Maybe t)

Methods

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

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

Apply a => Apply (Ptr a)

Methods

apply :: Ptr a -> Args -> Ptr a

applyE :: Ptr a -> Elims -> Ptr a

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)