Agda-2.5.2: A dependently typed functional programming language and proof assistant

Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.MetaVars.Mention

Documentation

class MentionsMeta t where Source #

Minimal complete definition

Methods

mentionsMeta :: MetaId -> t -> Bool Source #

Instances

MentionsMeta LevelAtom Source #
Methods mentionsMeta :: MetaId -> LevelAtom -> Bool Source #
MentionsMeta PlusLevel Source #
Methods mentionsMeta :: MetaId -> PlusLevel -> Bool Source #
MentionsMeta Level Source #
Methods mentionsMeta :: MetaId -> Level -> Bool Source #
MentionsMeta Sort Source #
Methods mentionsMeta :: MetaId -> Sort -> Bool Source #
MentionsMeta Type Source #
Methods mentionsMeta :: MetaId -> Type -> Bool Source #
MentionsMeta Elim Source #
Methods mentionsMeta :: MetaId -> Elim -> Bool Source #
MentionsMeta Term Source #
Methods mentionsMeta :: MetaId -> Term -> Bool Source #
MentionsMeta Constraint Source #
Methods mentionsMeta :: MetaId -> Constraint -> Bool Source #
MentionsMeta ProblemConstraint Source #
Methods mentionsMeta :: MetaId -> ProblemConstraint -> Bool Source #
MentionsMeta t => MentionsMeta [t] Source #
Methods mentionsMeta :: MetaId -> [t] -> Bool Source #
MentionsMeta t => MentionsMeta (Maybe t) Source #
Methods mentionsMeta :: MetaId -> Maybe t -> Bool Source #
MentionsMeta t => MentionsMeta (Dom t) Source #
Methods mentionsMeta :: MetaId -> Dom t -> Bool Source #
MentionsMeta t => MentionsMeta (Arg t) Source #
Methods mentionsMeta :: MetaId -> Arg t -> Bool Source #
MentionsMeta a => MentionsMeta (Tele a) Source #
Methods mentionsMeta :: MetaId -> Tele a -> Bool Source #
MentionsMeta t => MentionsMeta (Abs t) Source #
Methods mentionsMeta :: MetaId -> Abs t -> Bool Source #
MentionsMeta a => MentionsMeta (Closure a) Source #
Methods mentionsMeta :: MetaId -> Closure a -> Bool Source #
(MentionsMeta a, MentionsMeta b) => MentionsMeta (a, b) Source #
Methods mentionsMeta :: MetaId -> (a, b) -> Bool Source #
(MentionsMeta a, MentionsMeta b, MentionsMeta c) => MentionsMeta (a, b, c) Source #
Methods mentionsMeta :: MetaId -> (a, b, c) -> Bool Source #