| Safe Haskell | None |
|---|
Agda.TypeChecking.MetaVars.Mention
Documentation
class MentionsMeta t whereSource
Methods
mentionsMeta :: MetaId -> t -> BoolSource
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 a => MentionsMeta (Tele a) | |
| MentionsMeta t => MentionsMeta (Abs t) | |
| MentionsMeta t => MentionsMeta (Dom t) | |
| MentionsMeta t => MentionsMeta (Arg t) | |
| MentionsMeta a => MentionsMeta (Closure a) | |
| (MentionsMeta a, MentionsMeta b) => MentionsMeta (a, b) | |
| (MentionsMeta a, MentionsMeta b, MentionsMeta c) => MentionsMeta (a, b, c) |