IsPrefixOf Elims Source # | |
Instance detailsDefined in Agda.TypeChecking.Abstract |
CheckInternal Elims Source # | |
Instance detailsDefined in Agda.TypeChecking.CheckInternal |
MentionsMeta Elim Source # | |
Instance detailsDefined in Agda.TypeChecking.MetaVars.Mention |
Occurs Elims Source # | |
Instance detailsDefined in Agda.TypeChecking.MetaVars.Occurs |
PrettyTCM Elim Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
Reduce Elim Source # | |
Instance detailsDefined in Agda.TypeChecking.Reduce |
Foldable Elim' Source # | |
Instance detailsDefined in Agda.Syntax.Internal.Elim |
Traversable Elim' Source # | |
Instance detailsDefined in Agda.Syntax.Internal.Elim |
Functor Elim' Source # | |
Instance detailsDefined in Agda.Syntax.Internal.Elim |
PatternFrom Elims [Elim' NLPat] Source # | |
Instance detailsDefined in Agda.TypeChecking.Rewriting.NonLinPattern |
LensOrigin (Elim' a) Source # | This instance cheats on Proj , use with care.
Proj s are always assumed to be UserWritten , since they have no ArgInfo .
Same for IApply |
Instance detailsDefined in Agda.Syntax.Internal.Elim |
Pretty tm => Pretty (Elim' tm) Source # | |
Instance detailsDefined in Agda.Syntax.Internal.Elim |
GetDefs a => GetDefs (Elim' a) Source # | |
Instance detailsDefined in Agda.Syntax.Internal.Defs |
IsProjElim (Elim' a) Source # | |
Instance detailsDefined in Agda.Syntax.Internal.Elim |
TermLike a => TermLike (Elim' a) Source # | |
Instance detailsDefined in Agda.Syntax.Internal.Generic |
TermLike a => AllMetas (Elim' a) Source # | |
Instance detailsDefined in Agda.Syntax.Internal.MetaVars |
NamesIn a => NamesIn (Elim' a) Source # | |
Instance detailsDefined in Agda.Syntax.Internal.Names |
KillRange a => KillRange (Elim' a) Source # | |
Instance detailsDefined in Agda.Syntax.Internal.Elim |
Reify i => Reify (Elim' i) Source # | |
Instance detailsDefined in Agda.Syntax.Translation.InternalToAbstract |
AbsTerm a => AbsTerm (Elim' a) Source # | |
Instance detailsDefined in Agda.TypeChecking.Abstract |
EqualSy a => EqualSy (Elim' a) Source # | |
Instance detailsDefined in Agda.TypeChecking.Abstract |
Free t => Free (Elim' t) Source # | |
Instance detailsDefined in Agda.TypeChecking.Free.Lazy |
PrecomputeFreeVars a => PrecomputeFreeVars (Elim' a) Source # | |
Instance detailsDefined in Agda.TypeChecking.Free.Precompute |
(Reduce a, ForceNotFree a) => ForceNotFree (Elim' a) Source # | |
Instance detailsDefined in Agda.TypeChecking.Free.Reduce |
UsableModality a => UsableModality (Elim' a) Source # | |
Instance detailsDefined in Agda.TypeChecking.Irrelevance |
UsableRelevance a => UsableRelevance (Elim' a) Source # | |
Instance detailsDefined in Agda.TypeChecking.Irrelevance |
AnyRigid a => AnyRigid (Elim' a) Source # | |
Instance detailsDefined in Agda.TypeChecking.MetaVars.Occurs |
ComputeOccurrences a => ComputeOccurrences (Elim' a) Source # | |
Instance detailsDefined in Agda.TypeChecking.Positivity |
PrettyTCM (Elim' DisplayTerm) Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM (Elim' NLPat) Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
Instantiate t => Instantiate (Elim' t) Source # | |
Instance detailsDefined in Agda.TypeChecking.Reduce |
InstantiateFull t => InstantiateFull (Elim' t) Source # | |
Instance detailsDefined in Agda.TypeChecking.Reduce |
IsMeta a => IsMeta (Elim' a) Source # | |
Instance detailsDefined in Agda.TypeChecking.Reduce |
Normalise t => Normalise (Elim' t) Source # | |
Instance detailsDefined in Agda.TypeChecking.Reduce |
Simplify t => Simplify (Elim' t) Source # | |
Instance detailsDefined in Agda.TypeChecking.Reduce |
GetMatchables a => GetMatchables (Elim' a) Source # | |
Instance detailsDefined in Agda.TypeChecking.Rewriting.NonLinPattern |
EmbPrj a => EmbPrj (Elim' a) Source # | |
Instance detailsDefined in Agda.TypeChecking.Serialise.Instances.Internal |
Subst a => Subst (Elim' a) Source # | |
Instance detailsDefined in Agda.TypeChecking.Substitute |
SynEq a => SynEq (Elim' a) Source # | |
Instance detailsDefined in Agda.TypeChecking.SyntacticEquality |
Show a => Show (Elim' a) Source # | |
Instance detailsDefined in Agda.Syntax.Internal.Elim |
NFData a => NFData (Elim' a) Source # | |
Instance detailsDefined in Agda.Syntax.Internal.Elim |
(Subst a, Eq a) => Eq (Elim' a) Source # | |
Instance detailsDefined in Agda.TypeChecking.Substitute |
(Subst a, Ord a) => Ord (Elim' a) Source # | |
Instance detailsDefined in Agda.TypeChecking.Substitute |
Match [Elim' NLPat] Elims Source # | |
Instance detailsDefined in Agda.TypeChecking.Rewriting.NonLinMatch |
ToNLPat (Arg DeBruijnPattern) (Elim' NLPat) Source # | |
Instance detailsDefined in Agda.TypeChecking.Rewriting.Clause |
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source # | |
Instance detailsDefined in Agda.TypeChecking.Rewriting.Clause |
ToNLPat a b => ToNLPat (Elim' a) (Elim' b) Source # | |
Instance detailsDefined in Agda.TypeChecking.Rewriting.Clause |
NLPatToTerm p a => NLPatToTerm (Elim' p) (Elim' a) Source # | |
Instance detailsDefined in Agda.TypeChecking.Rewriting.NonLinPattern |
type TypeOf Elims Source # | |
Instance detailsDefined in Agda.Syntax.Internal |
type TypeOf [Elim' NLPat] Source # | |
Instance detailsDefined in Agda.TypeChecking.Monad.Base |
type ReifiesTo (Elim' i) Source # | |
Instance detailsDefined in Agda.Syntax.Translation.InternalToAbstract |
type SubstArg (Elim' a) Source # | |
Instance detailsDefined in Agda.TypeChecking.Substitute |