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

Agda.TypeChecking.Substitute

Description

This module contains the definition of hereditary substitution and application operating on internal syntax which is in β-normal form (β including projection reductions).

Further, it contains auxiliary functions which rely on substitution but not on reduction.

Synopsis

Documentation

class TeleNoAbs a where Source #

Performs void (noAbs) abstraction over telescope.

Methods

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

Instances

Instances details
TeleNoAbs ListTel Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

teleNoAbs :: ListTel -> Term -> Term Source #

TeleNoAbs Telescope Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

data TelV a Source #

Constructors

TelV 

Fields

Instances

Instances details
Functor TelV Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Methods

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

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

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

applyTermE :: forall t. (Coercible Term t, Apply t, Subst t t) => (Empty -> Term -> Elims -> Term) -> t -> Elims -> t Source #

Apply Elims while using the given function to report ill-typed redexes. Recursive calls for applyE and applySubst happen at type t to propagate the same strategy to subtrees.

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

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

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

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

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

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

telView' :: Type -> TelView Source #

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

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

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

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.

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

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

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 #

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

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

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

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

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

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

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

data Substitution' a Source #

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

Instances details
Eq Substitution Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Functor Substitution' Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

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

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

Ord Substitution Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Foldable Substitution' Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

fold :: Monoid m => Substitution' m -> m #

foldMap :: Monoid m => (a -> m) -> Substitution' a -> m #

foldMap' :: Monoid m => (a -> m) -> Substitution' a -> m #

foldr :: (a -> b -> b) -> b -> Substitution' a -> b #

foldr' :: (a -> b -> b) -> b -> Substitution' a -> b #

foldl :: (b -> a -> b) -> b -> Substitution' a -> b #

foldl' :: (b -> a -> b) -> b -> Substitution' a -> b #

foldr1 :: (a -> a -> a) -> Substitution' a -> a #

foldl1 :: (a -> a -> a) -> Substitution' a -> a #

toList :: Substitution' a -> [a] #

null :: Substitution' a -> Bool #

length :: Substitution' a -> Int #

elem :: Eq a => a -> Substitution' a -> Bool #

maximum :: Ord a => Substitution' a -> a #

minimum :: Ord a => Substitution' a -> a #

sum :: Num a => Substitution' a -> a #

product :: Num a => Substitution' a -> a #

Traversable Substitution' Source # 
Instance details

Defined in Agda.Syntax.Internal

Methods

traverse :: Applicative f => (a -> f b) -> Substitution' a -> f (Substitution' b) #

sequenceA :: Applicative f => Substitution' (f a) -> f (Substitution' a) #

mapM :: Monad m => (a -> m b) -> Substitution' a -> m (Substitution' b) #

sequence :: Monad m => Substitution' (m a) -> m (Substitution' a) #

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

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

Defined in Agda.Syntax.Internal

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

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

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

Defined in Agda.TypeChecking.Pretty

Orphan instances

Eq Substitution Source # 
Instance details

Eq NotBlocked Source # 
Instance details

Eq LevelAtom Source # 
Instance details

Eq PlusLevel Source # 
Instance details

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

Eq Section Source # 
Instance details

Methods

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

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

Eq CompareAs Source # 
Instance details

Ord Substitution Source # 
Instance details

Ord LevelAtom Source # 
Instance details

Ord PlusLevel Source # 
Instance details

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

DeBruijn NLPat Source # 
Instance details

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

Subst Term () Source # 
Instance details

Methods

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

Subst Term String Source # 
Instance details

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

Subst Term Constraint Source # 
Instance details

Subst NLPat RewriteRule Source # 
Instance details

Subst NLPat NLPSort Source # 
Instance details

Subst NLPat NLPType Source # 
Instance details

Subst NLPat NLPat Source # 
Instance details

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

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

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

(Coercible a Term, Subst t a) => Subst t (Sort' a) Source # 
Instance details

Methods

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

Subst a a => Subst a (Substitution' 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 b) => Subst t (Dom' a b) Source # 
Instance details

Methods

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

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

Methods

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

(Coercible a Term, Subst t a, Subst t b) => Subst t (Type'' a b) Source # 
Instance details

Methods

applySubst :: Substitution' t -> Type'' a b -> Type'' a b 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 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 #

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

Ord a => Ord (Dom a) Source # 
Instance details

Methods

compare :: Dom a -> Dom a -> Ordering #

(<) :: Dom a -> Dom a -> Bool #

(<=) :: Dom a -> Dom a -> Bool #

(>) :: Dom a -> Dom a -> Bool #

(>=) :: Dom a -> Dom a -> Bool #

max :: Dom a -> Dom a -> Dom a #

min :: Dom a -> Dom a -> Dom a #

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

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

Methods

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

Abstract [Polarity] Source # 
Instance details

Abstract [Occurrence] 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 [Polarity] Source # 
Instance details

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

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 #