← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to src/full/Agda/TypeChecking/MetaVars/Mention.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/TypeChecking/MetaVars/Mention.hs
1
 
 
 
1
{-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}
2
2
module Agda.TypeChecking.MetaVars.Mention where
3
3
 
4
 
import Data.Traversable
5
 
 
6
4
import Agda.Syntax.Common
7
 
import Agda.Syntax.Internal
8
 
import Agda.TypeChecking.Reduce
 
5
import Agda.Syntax.Internal as I
9
6
import Agda.TypeChecking.Monad
10
7
 
11
8
 
55
52
instance MentionsMeta t => MentionsMeta (Abs t) where
56
53
  mentionsMeta x = mentionsMeta x . unAbs
57
54
 
58
 
instance MentionsMeta t => MentionsMeta (Arg t) where
59
 
  mentionsMeta x (Arg h Irrelevant t) = False  -- we don't have to look inside irrelevant arguments when deciding to wake constraints
 
55
instance MentionsMeta t => MentionsMeta (I.Arg t) where
 
56
  mentionsMeta x a | isIrrelevant a = False
 
57
  -- ^ we don't have to look inside irrelevant arguments when deciding to wake constraints
60
58
  mentionsMeta x a = mentionsMeta x (unArg a)
61
59
 
62
 
instance MentionsMeta t => MentionsMeta (Dom t) where
 
60
instance MentionsMeta t => MentionsMeta (I.Dom t) where
63
61
  mentionsMeta x = mentionsMeta x . unDom
64
62
 
65
63
instance MentionsMeta t => MentionsMeta [t] where
107
105
 
108
106
-- instance (Ord k, MentionsMeta e) => MentionsMeta (Map k e) where
109
107
--   mentionsMeta = traverse mentionsMeta
110