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

Safe Haskell | None

Agda.TypeChecking.MetaVars.Mention

# Documentation

class MentionsMeta t where

Methods

mentionsMeta :: MetaId -> t -> Bool

Instances

MentionsMeta LevelAtom |
MentionsMeta PlusLevel |
MentionsMeta Level |
MentionsMeta Sort |
MentionsMeta Type |
MentionsMeta Elim |
MentionsMeta Term |
MentionsMeta Constraint |
MentionsMeta ProblemConstraint |
MentionsMeta t => MentionsMeta [t] |
MentionsMeta t => MentionsMeta (Maybe t) |
MentionsMeta t => MentionsMeta (Arg t) |
MentionsMeta t => MentionsMeta (Dom t) |
MentionsMeta a => MentionsMeta (Tele a) |
MentionsMeta t => MentionsMeta (Abs t) |
MentionsMeta a => MentionsMeta (Closure a) |
(MentionsMeta a, MentionsMeta b) => MentionsMeta (a, b) |
(MentionsMeta a, MentionsMeta b, MentionsMeta c) => MentionsMeta (a, b, c) |