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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.MetaVars.Mention

# Documentation

class MentionsMeta t where Source #

Methods

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

#### Instances

Instances details

MentionsMeta Elim Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Elim -> Bool Source #
MentionsMeta Level Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Level -> Bool Source #
MentionsMeta PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> PlusLevel -> Bool Source #
MentionsMeta Sort Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Sort -> Bool Source #
MentionsMeta Term Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Term -> Bool Source #
MentionsMeta Type Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Type -> Bool Source #
MentionsMeta Blocker Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Blocker -> Bool Source #
MentionsMeta CompareAs Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> CompareAs -> Bool Source #
MentionsMeta Constraint Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Constraint -> Bool Source #
MentionsMeta ProblemConstraint Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> ProblemConstraint -> Bool Source #
MentionsMeta t => MentionsMeta (Arg t) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Arg t -> Bool Source #
MentionsMeta t => MentionsMeta (Abs t) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Abs t -> Bool Source #
MentionsMeta t => MentionsMeta (Dom t) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Dom t -> Bool Source #
MentionsMeta a => MentionsMeta (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Tele a -> Bool Source #
MentionsMeta a => MentionsMeta (Closure a) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Closure a -> Bool Source #
MentionsMeta t => MentionsMeta (Maybe t) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Maybe t -> Bool Source #
MentionsMeta t => MentionsMeta [t] Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> [t] -> Bool Source #
(MentionsMeta a, MentionsMeta b) => MentionsMeta (a, b) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> (a, b) -> Bool Source #
(MentionsMeta a, MentionsMeta b, MentionsMeta c) => MentionsMeta (a, b, c) Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> (a, b, c) -> Bool Source #

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