1 files changed, 67 insertions, 0 deletions
diff --git a/src/CC/Name.idr b/src/CC/Name.idr
new file mode 100644
index 0000000..f1a66db
--- /dev/null
+++ b/src/CC/Name.idr
@@ -0,0 +1,67 @@
+module CC.Name
+
+import Control.Relation
+
+import Decidable.Equality
+
+import Text.Bounded
+import Text.PrettyPrint.Prettyprinter
+
+infix 4 ~~
+
+-- Definitions -----------------------------------------------------------------
+
+||| Names of variables.
+export
+Name : Type
+Name = WithBounds String
+
+%name Name n, m
+
+||| Equivalence relation on names.
+export
+(~~) : Rel Name
+m ~~ n = m.val = n.val
+
+%name (~~) prf
+
+-- Interfaces ------------------------------------------------------------------
+
+export
+Interpolation Name where
+  interpolate n = n.val
+
+export
+Pretty Name where
+  pretty n = pretty n.val
+
+export
+Reflexive Name (~~) where
+  reflexive = Refl
+
+export
+Symmetric Name (~~) where
+  symmetric prf = sym prf
+
+export
+Transitive Name (~~) where
+  transitive prf1 prf2 = trans prf1 prf2
+
+export Equivalence Name (~~) where
+
+-- Operations ------------------------------------------------------------------
+
+||| Constructs a new name from a bounded String.
+export
+MkName : WithBounds String -> Name
+MkName = id
+
+||| Decides if two names are equivalent
+export
+decEquiv : (m, n : Name) -> Dec (m ~~ n)
+decEquiv m n = decEq m.val n.val
+
+||| Returns the bounds of `name`, if any.
+export
+bounds : (name : Name) -> Maybe Bounds
+bounds name = if name.isIrrelevant then Nothing else Just name.bounds