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

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.MetaVars.Mention

Documentation

class MentionsMeta t where Source #

Methods

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

Instances
MentionsMeta LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

MentionsMeta PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

MentionsMeta Level Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

MentionsMeta Sort Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

MentionsMeta Type Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

MentionsMeta Elim Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

MentionsMeta Term Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

MentionsMeta Constraint Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

MentionsMeta ProblemConstraint Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

MentionsMeta t => MentionsMeta [t] Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

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

MentionsMeta t => MentionsMeta (Maybe t) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

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

MentionsMeta t => MentionsMeta (Dom t) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

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

MentionsMeta t => MentionsMeta (Arg t) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

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

MentionsMeta a => MentionsMeta (Tele a) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMeta :: MetaId -> Tele a -> Bool Source #

MentionsMeta t => MentionsMeta (Abs t) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

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

MentionsMeta a => MentionsMeta (Closure a) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

(MentionsMeta a, MentionsMeta b) => MentionsMeta (a, b) Source # 
Instance details

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMeta :: 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

mentionsMeta :: MetaId -> (a, b, c) -> Bool Source #