Agda-2.6.2.1.20220320: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.Internal.Elim

Synopsis

Documentation

data Elim' a Source #

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

Instances

Instances details
IsPrefixOf Elims Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

MentionsMeta Elim Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Elim -> Bool Source #

PrettyTCM Elim Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Elim -> m Doc Source #

Reduce Elim Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Foldable Elim' Source # 
Instance details

Defined in Agda.Syntax.Internal.Elim

Methods

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

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

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

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

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

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

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

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

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

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

null :: Elim' a -> Bool #

length :: Elim' a -> Int #

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

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

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

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

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

Traversable Elim' Source # 
Instance details

Defined in Agda.Syntax.Internal.Elim

Methods

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

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

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

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

Functor Elim' Source # 
Instance details

Defined in Agda.Syntax.Internal.Elim

Methods

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

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

LensOrigin (Elim' a) Source #

This instance cheats on Proj, use with care. Projs are always assumed to be UserWritten, since they have no ArgInfo. Same for IApply

Instance details

Defined in Agda.Syntax.Internal.Elim

GetDefs a => GetDefs (Elim' a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Defs

Methods

getDefs :: MonadGetDefs m => Elim' a -> m () Source #

IsProjElim (Elim' a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Elim

TermLike a => TermLike (Elim' a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Elim' a -> m (Elim' a) Source #

foldTerm :: Monoid m => (Term -> m) -> Elim' a -> m Source #

TermLike a => AllMetas (Elim' a) Source # 
Instance details

Defined in Agda.Syntax.Internal.MetaVars

Methods

allMetas :: Monoid m => (MetaId -> m) -> Elim' a -> m Source #

NamesIn a => NamesIn (Elim' a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

namesIn' :: Monoid m => (QName -> m) -> Elim' a -> m Source #

KillRange a => KillRange (Elim' a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Elim

Reify i => Reify (Elim' i) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (Elim' i) Source #

Methods

reify :: MonadReify m => Elim' i -> m (ReifiesTo (Elim' i)) Source #

reifyWhen :: MonadReify m => Bool -> Elim' i -> m (ReifiesTo (Elim' i)) Source #

AbsTerm a => AbsTerm (Elim' a) Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

absTerm :: Term -> Elim' a -> Elim' a Source #

EqualSy a => EqualSy (Elim' a) Source # 
Instance details

Defined in Agda.TypeChecking.Abstract

Methods

equalSy :: Elim' a -> Elim' a -> Bool Source #

Free t => Free (Elim' t) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet a c => Elim' t -> FreeM a c Source #

PrecomputeFreeVars a => PrecomputeFreeVars (Elim' a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: Elim' a -> FV (Elim' a) Source #

(Reduce a, ForceNotFree a) => ForceNotFree (Elim' a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Reduce

Methods

forceNotFree' :: MonadFreeRed m => Elim' a -> m (Elim' a)

UsableModality a => UsableModality (Elim' a) Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

UsableRelevance a => UsableRelevance (Elim' a) Source # 
Instance details

Defined in Agda.TypeChecking.Irrelevance

AnyRigid a => AnyRigid (Elim' a) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

anyRigid :: PureTCM tcm => (Nat -> tcm Bool) -> Elim' a -> tcm Bool Source #

Occurs a => Occurs (Elim' a) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Occurs

Methods

occurs :: Elim' a -> OccursM (Elim' a) Source #

metaOccurs :: MetaId -> Elim' a -> TCM () Source #

ComputeOccurrences a => ComputeOccurrences (Elim' a) Source # 
Instance details

Defined in Agda.TypeChecking.Positivity

PrettyTCM (Elim' DisplayTerm) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

PrettyTCM (Elim' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Pretty

Instantiate t => Instantiate (Elim' t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Elim' t -> ReduceM (Elim' t) Source #

InstantiateFull t => InstantiateFull (Elim' t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

IsMeta a => IsMeta (Elim' a) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

isMeta :: Elim' a -> Maybe MetaId Source #

Normalise t => Normalise (Elim' t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

normalise' :: Elim' t -> ReduceM (Elim' t) Source #

Simplify t => Simplify (Elim' t) Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Methods

simplify' :: Elim' t -> ReduceM (Elim' t) Source #

GetMatchables a => GetMatchables (Elim' a) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

getMatchables :: Elim' a -> [QName] Source #

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

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

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

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

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

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

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Elim' a) Source #

SynEq a => SynEq (Elim' a) Source # 
Instance details

Defined in Agda.TypeChecking.SyntacticEquality

Methods

synEq :: Elim' a -> Elim' a -> SynEqM (Elim' a, Elim' a)

synEq' :: Elim' a -> Elim' a -> SynEqM (Elim' a, Elim' a)

Pretty tm => Pretty (Elim' tm) Source # 
Instance details

Defined in Agda.Syntax.Internal.Elim

Methods

pretty :: Elim' tm -> Doc Source #

prettyPrec :: Int -> Elim' tm -> Doc Source #

prettyList :: [Elim' tm] -> Doc Source #

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

Defined in Agda.Syntax.Internal.Elim

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Elim' a -> c (Elim' a) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Elim' a) #

toConstr :: Elim' a -> Constr #

dataTypeOf :: Elim' a -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Elim' a)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Elim' a)) #

gmapT :: (forall b. Data b => b -> b) -> Elim' a -> Elim' a #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Elim' a -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Elim' a -> r #

gmapQ :: (forall d. Data d => d -> u) -> Elim' a -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Elim' a -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Elim' a -> m (Elim' a) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Elim' a -> m (Elim' a) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Elim' a -> m (Elim' a) #

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

Defined in Agda.Syntax.Internal.Elim

Methods

showsPrec :: Int -> Elim' a -> ShowS #

show :: Elim' a -> String #

showList :: [Elim' a] -> ShowS #

NFData a => NFData (Elim' a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Elim

Methods

rnf :: Elim' a -> () #

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

Defined in Agda.TypeChecking.Substitute

Methods

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

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

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

Defined in Agda.TypeChecking.Substitute

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 #

ToNLPat (Arg DeBruijnPattern) (Elim' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.Clause

ToNLPat (NamedArg DeBruijnPattern) (Elim' NLPat) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.Clause

ToNLPat a b => ToNLPat (Elim' a) (Elim' b) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.Clause

Methods

toNLPat :: Elim' a -> Elim' b Source #

NLPatToTerm p a => NLPatToTerm (Elim' p) (Elim' a) Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Methods

nlPatToTerm :: PureTCM m => Elim' p -> m (Elim' a) Source #

PatternFrom (Type, Term) Elims [Elim' NLPat] Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinPattern

Match (Type, Elims -> Term) [Elim' NLPat] Elims Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

match :: Relevance -> Telescope -> Telescope -> (Type, Elims -> Term) -> [Elim' NLPat] -> Elims -> NLM () Source #

type ReifiesTo (Elim' i) Source # 
Instance details

Defined in Agda.Syntax.Translation.InternalToAbstract

type SubstArg (Elim' a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg (Elim' a) = SubstArg a

isApplyElim :: Elim' a -> Maybe (Arg a) Source #

Drop Apply constructor. (Safe)

allApplyElims :: [Elim' a] -> Maybe [Arg a] Source #

Drop Apply constructors. (Safe)

splitApplyElims :: [Elim' a] -> ([Arg a], [Elim' a]) Source #

Split at first non-Apply

class IsProjElim e where Source #

Instances

Instances details
IsProjElim (Elim' a) Source # 
Instance details

Defined in Agda.Syntax.Internal.Elim

IsProjElim e => IsProjElim (MaybeReduced e) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

argsFromElims :: [Elim' t] -> [Arg t] Source #

Discards Proj f entries.

allProjElims :: [Elim' t] -> Maybe [(ProjOrigin, QName)] Source #

Drop Proj constructors. (Safe)