Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Substitute

Contents

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

class TeleNoAbs a where Source #

Performs void (noAbs) abstraction over telescope.

Methods

teleNoAbs :: a -> Term -> Term Source #

Instances
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

data TelV a Source #

Constructors

TelV 

Fields

Instances
Functor TelV Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

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

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

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

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

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

conApp :: ConHead -> ConInfo -> Elims -> Elims -> Term Source #

Eliminate a constructed term.

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.

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.

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

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

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

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

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

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

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

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

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.

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

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

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

Uses free variable analysis to introduce NoAbs bindings.

telePi_ :: Telescope -> Type -> Type Source #

Everything will be an Abs.

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.

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

Get the next higher sort.

univSort :: Maybe Sort -> Sort -> Sort Source #

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

funSort' :: Sort -> Sort -> Maybe Sort Source #

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

piSort' :: Sort -> Abs Sort -> Maybe Sort Source #

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

data Substitution' a Source #

Substitutions.

Constructors

IdS

Identity substitution. Γ ⊢ IdS : Γ

EmptyS Empty

Empty substitution, lifts from the empty context. First argument is (throwImpossible (Impossible "srcfullAgdaSyntaxInternal.hs" 614)). 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 (throwImpossible (Impossible "srcfullAgdaSyntaxInternal.hs" 627)). 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' Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

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

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)

KillRange Substitution Source # 
Instance details

Defined in Agda.Syntax.Internal

InstantiateFull Substitution Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

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

Defined in Agda.TypeChecking.Substitute

Eq (Substitution' Term) 
Instance details

Defined in Agda.TypeChecking.Substitute

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

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

Ord (Substitution' Term) 
Instance details

Defined in Agda.TypeChecking.Substitute

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

Defined in Agda.Syntax.Internal

Methods

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

show :: Substitution' a -> String

showList :: [Substitution' a] -> ShowS

Null (Substitution' a) Source # 
Instance details

Defined in Agda.Syntax.Internal

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

Methods

termSize :: Substitution' a -> Int Source #

tsize :: Substitution' a -> Sum Int Source #

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

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

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

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

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

Defined in Agda.TypeChecking.Pretty

Orphan instances

Eq NotBlocked Source # 
Instance details

Methods

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

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

Eq LevelAtom Source # 
Instance details

Methods

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

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

Eq PlusLevel Source # 
Instance details

Methods

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

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

Eq Level Source # 
Instance details

Methods

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

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

Eq Sort Source # 
Instance details

Methods

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

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

Eq Term Source #

Syntactic Term equality, ignores stuff below DontCare and sharing.

Instance details

Methods

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

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

Eq Candidate Source # 
Instance details

Methods

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

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

Eq Section Source # 
Instance details

Methods

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

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

Eq Constraint Source # 
Instance details

Methods

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

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

Ord LevelAtom Source # 
Instance details

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 Source # 
Instance details

Methods

compare :: PlusLevel -> PlusLevel -> Ordering

(<) :: PlusLevel -> PlusLevel -> Bool

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

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

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

max :: PlusLevel -> PlusLevel -> PlusLevel

min :: PlusLevel -> PlusLevel -> PlusLevel

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

DeBruijn DeBruijnPattern Source # 
Instance details

DeBruijn NLPat Source # 
Instance details

Methods

deBruijnVar :: Int -> NLPat Source #

debruijnNamedVar :: String -> Int -> NLPat Source #

deBruijnView :: NLPat -> Maybe Int Source #

Abstract Permutation Source # 
Instance details

Abstract Clause Source # 
Instance details

Abstract Sort Source # 
Instance details

Abstract Telescope Source # 
Instance details

Abstract Type Source # 
Instance details

Abstract Term Source # 
Instance details

Abstract CompiledClauses Source # 
Instance details

Abstract FunctionInverse Source # 
Instance details

Abstract PrimFun Source # 
Instance details

Abstract Defn Source # 
Instance details

Abstract ProjLams Source # 
Instance details

Abstract Projection Source # 
Instance details

Abstract System Source # 
Instance details

Abstract NumGeneralizableArgs Source # 
Instance details

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

Apply Permutation 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 FunctionInverse Source # 
Instance details

Apply PrimFun Source # 
Instance details

Apply Defn Source # 
Instance details

Methods

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

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

Apply ProjLams Source # 
Instance details

Apply Projection Source # 
Instance details

Apply ExtLamInfo Source # 
Instance details

Apply System Source # 
Instance details

Apply NumGeneralizableArgs Source # 
Instance details

Apply Definition Source # 
Instance details

Apply RewriteRule Source # 
Instance details

Apply DisplayTerm Source # 
Instance details

Subst DeBruijnPattern DeBruijnPattern Source # 
Instance details

Subst Term () Source # 
Instance details

Methods

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

Subst Term String Source # 
Instance details

Methods

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

Subst Term Range Source # 
Instance details

Subst Term Name Source # 
Instance details

Subst Term EqualityView Source # 
Instance details

Subst Term ConPatternInfo Source # 
Instance details

Subst Term Pattern Source # 
Instance details

Subst Term LevelAtom Source # 
Instance details

Subst Term PlusLevel Source # 
Instance details

Subst Term Level Source # 
Instance details

Subst Term Sort Source # 
Instance details

Subst Term Term Source # 
Instance details

Subst Term ProblemEq Source # 
Instance details

Subst Term Candidate Source # 
Instance details

Subst Term DisplayTerm Source # 
Instance details

Subst Term DisplayForm Source # 
Instance details

Subst Term Constraint Source # 
Instance details

Subst NLPat RewriteRule Source # 
Instance details

Subst NLPat NLPType Source # 
Instance details

Subst NLPat NLPat Source # 
Instance details

Subst t a => Subst t [a] Source # 
Instance details

Methods

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

Subst t a => Subst t (Maybe a) Source # 
Instance details

Methods

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

Subst t a => Subst t (Dom a) Source # 
Instance details

Methods

applySubst :: Substitution' t -> Dom a -> Dom a Source #

Subst t a => Subst t (Arg a) Source # 
Instance details

Methods

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

Subst t a => Subst t (Abs a) Source # 
Instance details

Methods

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

Subst t a => Subst t (Elim' a) Source # 
Instance details

Methods

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

Subst t a => Subst t (Tele a) Source # 
Instance details

Methods

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

Subst t a => Subst t (Blocked a) Source # 
Instance details

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

Subst Term a => Subst Term (Type' a) Source # 
Instance details

(Subst t a, Subst t b) => Subst t (a, b) Source # 
Instance details

Methods

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

(Ord k, Subst t a) => Subst t (Map k a) Source # 
Instance details

Methods

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

Subst t a => Subst t (Named name a) Source # 
Instance details

Methods

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

(Subst t a, Subst t b, Subst t c) => Subst t (a, b, c) Source # 
Instance details

Methods

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

(Subst t a, Subst t b, Subst t c, Subst t d) => Subst t (a, b, c, d) Source # 
Instance details

Methods

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

Eq (Substitution' Term) Source # 
Instance details

Eq a => Eq (Pattern' a) Source # 
Instance details

Methods

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

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

Eq t => Eq (Blocked t) Source # 
Instance details

Methods

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

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

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

(Subst t a, Eq a) => Eq (Elim' a) Source # 
Instance details

Methods

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

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

Ord (Substitution' Term) Source # 
Instance details

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

(Subst t 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 t => Abstract [t] Source # 
Instance details

Methods

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

Abstract [Occurrence] Source # 
Instance details

Abstract [Polarity] Source # 
Instance details

Abstract t => Abstract (Maybe t) Source # 
Instance details

Methods

abstract :: Telescope -> Maybe t -> Maybe t Source #

DoDrop a => Abstract (Drop a) Source # 
Instance details

Methods

abstract :: Telescope -> Drop a -> Drop a Source #

Abstract a => Abstract (Case a) Source # 
Instance details

Methods

abstract :: Telescope -> Case a -> Case a Source #

Abstract a => Abstract (WithArity a) Source # 
Instance details

Apply t => Apply [t] Source # 
Instance details

Methods

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

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

Apply [NamedArg (Pattern' a)] Source #

Make sure we only drop variable patterns.

Instance details

Apply [Occurrence] Source # 
Instance details

Apply [Polarity] Source # 
Instance details

Apply t => Apply (Maybe t) Source # 
Instance details

Methods

apply :: Maybe t -> Args -> Maybe t Source #

applyE :: Maybe t -> Elims -> Maybe t Source #

DoDrop a => Apply (Drop a) Source # 
Instance details

Methods

apply :: Drop a -> Args -> Drop a Source #

applyE :: Drop a -> Elims -> Drop a Source #

Apply t => Apply (Blocked t) Source # 
Instance details

Methods

apply :: Blocked t -> Args -> Blocked t Source #

applyE :: Blocked t -> Elims -> Blocked t Source #

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

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 a, Apply b) => Apply (a, b) Source # 
Instance details

Methods

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

applyE :: (a, b) -> Elims -> (a, b) 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 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 #