Agda.Syntax.Internal.Elim · Agda-2.7.0.1

datadata Elim' a

#

Eliminations, subsuming applications and projections.

Constructors

Apply (Arg a)
Application.
Proj ProjOrigin QName
Projection. QName is name of a record projection.
IApply a a a
IApply x y r, x and y are the endpoints

Instances61Functor, Foldable, Traversable, Reduce, StripAllProjections, IsPrefixOf, …

Functor Elim'Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Elim
Foldable Elim'Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Elim
Traversable Elim'Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Elim
PrettyTCM ElimDefined in Agda-2.7.0.1 · Agda.TypeChecking.Pretty
Reduce ElimDefined in Agda-2.7.0.1 · Agda.TypeChecking.Reduce
StripAllProjections ElimsDefined in Agda-2.7.0.1 · Agda.Termination.TermCheck
IsPrefixOf ElimsDefined in Agda-2.7.0.1 · Agda.TypeChecking.Abstract
CheckInternal ElimsDefined in Agda-2.7.0.1 · Agda.TypeChecking.CheckInternal
MentionsMeta ElimDefined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Mention
Occurs ElimsDefined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs
AllHoles ElimsDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.Confluence
PatternFrom Elims [Elim' NLPat]Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinPattern
(Subst a, Eq a) => Eq (Elim' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Substitute · orphan
(Subst a, Ord a) => Ord (Elim' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Substitute · orphan
Show a => Show (Elim' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Elim
NFData a => NFData (Elim' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Elim
Pretty tm => Pretty (Elim' tm)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Elim
Subst a => Subst (Elim' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Substitute · orphan
PrettyTCM (Elim' DisplayTerm)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Pretty
PrettyTCM (Elim' NLPat)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Pretty
Reify i => Reify (Elim' i)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.InternalToAbstract
Simplify t => Simplify (Elim' t)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Reduce
Instantiate t => Instantiate (Elim' t)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Reduce
Normalise t => Normalise (Elim' t)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Reduce
KillRange a => KillRange (Elim' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Elim
LensOrigin (Elim' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Elim
This instance cheats on Proj, use with care. Projs are always assumed to be UserWritten, since they have no ArgInfo. Same for IApply
IsProjElim (Elim' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Elim
GetDefs a => GetDefs (Elim' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Defs
TermLike a => TermLike (Elim' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Generic
TermLike a => AllMetas (Elim' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.MetaVars
NamesIn a => NamesIn (Elim' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Names
Free t => Free (Elim' t)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Lazy
ExtractCalls a => ExtractCalls (Elim' a)Defined in Agda-2.7.0.1 · Agda.Termination.TermCheck
AbsTerm a => AbsTerm (Elim' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Abstract
EqualSy a => EqualSy (Elim' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Abstract
PrecomputeFreeVars a => PrecomputeFreeVars (Elim' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Precompute
IsMeta a => IsMeta (Elim' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Reduce
Match a => Match (Elim' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.DisplayForm
(SubstWithOrigin a, SubstWithOrigin (Arg a)) => SubstWithOrigin (Elim' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.DisplayForm
ForcedVariables a => ForcedVariables (Elim' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Forcing
(Reduce a, ForceNotFree a) => ForceNotFree (Elim' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Free.Reduce
UsableModality a => UsableModality (Elim' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Irrelevance
UsableRelevance a => UsableRelevance (Elim' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Irrelevance
AnyRigid a => AnyRigid (Elim' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.MetaVars.Occurs
HasPolarity a => HasPolarity (Elim' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Polarity
ComputeOccurrences a => ComputeOccurrences (Elim' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Positivity
InstantiateFull t => InstantiateFull (Elim' t)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Reduce
MetasToVars a => MetasToVars (Elim' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.Confluence
ParallelReduce a => ParallelReduce (Elim' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.Confluence
GetMatchables a => GetMatchables (Elim' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinPattern
EmbPrj a => EmbPrj (Elim' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Internal · orphan
SynEq a => SynEq (Elim' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SyntacticEquality
Match [Elim' NLPat] ElimsDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
ToNLPat (Arg DeBruijnPattern) (Elim' NLPat)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.Clause
ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.Clause
ToNLPat a b => ToNLPat (Elim' a) (Elim' b)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.Clause
NLPatToTerm p a => NLPatToTerm (Elim' p) (Elim' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinPattern
type SubstArg (Elim' a) = SubstArg aDefined in Agda-2.7.0.1 · Agda.TypeChecking.Substitute · orphan
type ReifiesTo (Elim' i) = Elim' (ReifiesTo i)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.InternalToAbstract
type TypeOf Elims = (Type, Elims -> Term)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal
type TypeOf [Elim' NLPat] = (Type, Elims -> Term)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Base

valueisApplyElim :: Elim' a -> Maybe (Arg a)

#

Drop Apply constructor. (Safe)

valueisApplyElim' :: Empty -> Elim' a -> Arg a

#

valueisProperApplyElim :: Elim' a -> Bool

#

Only Apply variant.

valueallApplyElims :: [Elim' a] -> Maybe [Arg a]

#

Drop Apply constructors. (Safe)

valuesplitApplyElims :: [Elim' a] -> ([Arg a], [Elim' a])

#

Split at first non-Apply

classclass IsProjElim e where

#

Methods

isProjElim :: e -> Maybe (ProjOrigin, QName)

Instances2IsProjElim

IsProjElim (Elim' a)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Elim
IsProjElim e => IsProjElim (MaybeReduced e)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Base

valueargsFromElims :: [Elim' t] -> [Arg t]

#

Discards Proj f entries.

valueallProjElims :: [Elim' t] -> Maybe [(ProjOrigin, QName)]

#

Drop Proj constructors. (Safe)