diff options
Diffstat (limited to 'src/Obs/NormalForm.idr')
| -rw-r--r-- | src/Obs/NormalForm.idr | 7 |
1 files changed, 4 insertions, 3 deletions
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 |