Eliminations, subsuming applications and projections.
Instances61Functor, Foldable, Traversable, Reduce, StripAllProjections, IsPrefixOf, …
Functor Elim'Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.ElimFoldable Elim'Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.ElimTraversable Elim'Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.ElimPrettyTCM ElimDefined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyReduce ElimDefined in Agda-2.8.0.2 · Agda.TypeChecking.ReduceStripAllProjections ElimsDefined in Agda-2.8.0.2 · Agda.Termination.TermCheckIsPrefixOf ElimsDefined in Agda-2.8.0.2 · Agda.TypeChecking.AbstractCheckInternal ElimsDefined in Agda-2.8.0.2 · Agda.TypeChecking.CheckInternalMentionsMeta ElimDefined in Agda-2.8.0.2 · Agda.TypeChecking.MetaVars.MentionOccurs ElimsDefined in Agda-2.8.0.2 · Agda.TypeChecking.MetaVars.OccursAllHoles ElimsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.ConfluencePatternFrom Elims [Elim' NLPat]Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.NonLinPattern(Subst a, Eq a) => Eq (Elim' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphan(Subst a, Ord a) => Ord (Elim' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphanShow a => Show (Elim' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.ElimNFData a => NFData (Elim' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.ElimPretty tm => Pretty (Elim' tm)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.ElimSubst a => Subst (Elim' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphanPrettyTCM (Elim' DisplayTerm)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyPrettyTCM (Elim' NLPat)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PrettyReify i => Reify (Elim' i)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstractSimplify t => Simplify (Elim' t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.ReduceInstantiate t => Instantiate (Elim' t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.ReduceNormalise t => Normalise (Elim' t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.ReduceFree t => Free (Elim' t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Free.LazyLensOrigin (Elim' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.ElimThis instance cheats on Proj, use with care. Projs are always assumed to be UserWritten, since they have no ArgInfo. Same for IApply
TermLike a => AllMetas (Elim' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.MetaVarsSynEq a => SynEq (Elim' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.SyntacticEqualityIsMeta a => IsMeta (Elim' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.ReduceTermLike a => TermLike (Elim' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.GenericAnyRigid a => AnyRigid (Elim' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.MetaVars.OccursKillRange a => KillRange (Elim' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.ElimIsProjElim (Elim' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.ElimGetDefs a => GetDefs (Elim' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.DefsNamesIn a => NamesIn (Elim' a)Defined in Agda-2.8.0.2 · Agda.Syntax.Internal.NamesExtractCalls a => ExtractCalls (Elim' a)Defined in Agda-2.8.0.2 · Agda.Termination.TermCheckAbsTerm a => AbsTerm (Elim' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.AbstractEqualSy a => EqualSy (Elim' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.AbstractPrecomputeFreeVars a => PrecomputeFreeVars (Elim' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Free.PrecomputeInstantiateFull t => InstantiateFull (Elim' t)Defined in Agda-2.8.0.2 · Agda.TypeChecking.ReduceMatch a => Match (Elim' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.DisplayForm(SubstWithOrigin a, SubstWithOrigin (Arg a)) => SubstWithOrigin (Elim' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.DisplayFormForcedVariables a => ForcedVariables (Elim' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Forcing(Reduce a, ForceNotFree a) => ForceNotFree (Elim' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Free.ReduceUsableModality a => UsableModality (Elim' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.IrrelevanceUsableRelevance a => UsableRelevance (Elim' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.IrrelevanceHasPolarity a => HasPolarity (Elim' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PolarityComputeOccurrences a => ComputeOccurrences (Elim' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.PositivityMetasToVars a => MetasToVars (Elim' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.ConfluenceParallelReduce a => ParallelReduce (Elim' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.ConfluenceGetMatchables a => GetMatchables (Elim' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.NonLinPatternEmbPrj a => EmbPrj (Elim' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Internal · orphanMatch [Elim' NLPat] ElimsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.NonLinMatchToNLPat (Arg DeBruijnPattern) (Elim' NLPat)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.ClauseToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.ClauseToNLPat a b => ToNLPat (Elim' a) (Elim' b)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.ClauseNLPatToTerm p a => NLPatToTerm (Elim' p) (Elim' a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.NonLinPatterntype SubstArg (Elim' a) = SubstArg aDefined in Agda-2.8.0.2 · Agda.TypeChecking.Substitute · orphantype ReifiesTo (Elim' i) = Elim' (ReifiesTo i)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.InternalToAbstracttype TypeOf Elims = (Type, Elims -> Term)Defined in Agda-2.8.0.2 · Agda.Syntax.Internaltype TypeOf [Elim' NLPat] = (Type, Elims -> Term)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base