diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-21 15:47:12 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-21 15:47:12 +0000 |
| commit | 4bad0e68e4b984db004d75ab87ca5a181d223190 (patch) | |
| tree | 95ac5fe8a30215c7c47cded8d017701b4095d02f /src/Obs/NormalForm.idr | |
| parent | cb4ec1e7c1551c1d28f00ba11b062daa78e8c4e3 (diff) | |
Improve parsing.
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 |