@@ -10,6 +10,7 @@ data TTName = UN String
1010 -- ^ Machine chosen names
1111 | NErased
1212 -- ^ Name of somethng which is never used in scope
13+%name TTName n, n'
1314
1415implicit
1516userSuppliedName : String -> TTName
@@ -19,6 +20,7 @@ data TTUExp = UVar Int
1920 -- ^ universe variable
2021 | UVal Int
2122 -- ^ explicit universe variable
23+%name TTUExp uexp
2224
2325-- | Primitive constants
2426data Const = I Int | BI Nat | Fl Float | Ch Char | Str String
@@ -27,6 +29,8 @@ data Const = I Int | BI Nat | Fl Float | Ch Char | Str String
2729 | B8Type | B16Type | B32Type | B64Type
2830 | PtrType | VoidType | Forgot
2931
32+%name Const c, c'
33+
3034abstract class ReflConst (a : Type) where
3135 toConst : a -> Const
3236
@@ -71,6 +75,7 @@ data NameType = Bound
7175 -- ^ constructor with tag and number
7276 | TCon Int Int
7377 -- ^ type constructor with tag and number
78+%name NameType nt, nt'
7479
7580-- | Types annotations for bound variables in different
7681-- binding contexts
@@ -83,7 +88,7 @@ data Binder a = Lam a
8388 | Guess a a
8489 | PVar a
8590 | PVTy a
86−
91+%name Binder b, b'
8792
8893instance Functor Binder where
8994 map f (Lam x) = Lam (f x)
@@ -139,6 +144,8 @@ data TT = P NameType TTName TT
139144 | TType TTUExp
140145 -- ^ types
141146
147+%name TT tm, tm'
148+
142149-- | Raw terms without types
143150data Raw = Var TTName
144151 | RBind TTName (Binder Raw) Raw
@@ -147,6 +154,8 @@ data Raw = Var TTName
147154 | RForce Raw
148155 | RConstant Const
149156
157+%name Raw tm, tm'
158+
150159data Tactic = Try Tactic Tactic
151160 -- ^ try the first tactic and resort to the second one on failure
152161 | GoalType String Tactic
@@ -185,4 +194,4 @@ data Tactic = Try Tactic Tactic
185194 -- ^ name a reflected term and type it
186195 | Compute
187196 -- ^ normalise the context
188−
197+%name Tactic tac, tac'