From 4bad0e68e4b984db004d75ab87ca5a181d223190 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Wed, 21 Dec 2022 15:47:12 +0000
Subject: Improve parsing.

---
 src/Obs/NormalForm.idr | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'src/Obs/NormalForm.idr')

diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index 2caf733..fd3a814 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -5,6 +5,7 @@ import Data.Fin
 import Obs.Sort
 import Obs.Substitution
 
+import Text.Bounded
 import Text.PrettyPrint.Prettyprinter
 
 %default total
@@ -49,7 +50,7 @@ data NormalForm : Nat -> Type where
 public export
 record Definition (n : Nat) where
   constructor MkDefinition
-  name   : String
+  name   : WithBounds String
   sort   : Sort
   ty     : NormalForm n
   tm     : NormalForm n
@@ -208,8 +209,8 @@ Pretty (NormalForm n) where
 export
 Pretty (Definition n) where
   pretty def = group $
-    pretty def.name <++> colon <+> softline <+> pretty def.ty <+> softline <+> colon <++> pretty def.sort <+> hardline <+>
-    pretty def.name <++> equals <+> softline <+> pretty def.tm
+    pretty def.name.val <++> colon <+> softline <+> pretty def.ty <+> softline <+> colon <++> pretty def.sort <+> hardline <+>
+    pretty def.name.val <++> equals <+> softline <+> pretty def.tm
 
 export
 Pretty (Context n) where
-- 
cgit v1.2.3