diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2023-01-07 22:01:05 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2023-01-07 22:01:05 +0000 |
| commit | eb49ef28b93431d9694a17b1ad44d9ea966bcb05 (patch) | |
| tree | 284683527022fb9a1d633a8a774532513d6630eb /src/Obs/Syntax.idr | |
| parent | ff65d1e285a97295708899bebdcc83ec214cd347 (diff) | |
Add postulates.
Diffstat (limited to 'src/Obs/Syntax.idr')
| -rw-r--r-- | src/Obs/Syntax.idr | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr index 868e761..ea7772e 100644 --- a/src/Obs/Syntax.idr +++ b/src/Obs/Syntax.idr @@ -72,6 +72,12 @@ record Definition where ty : WithBounds Syntax tm : WithBounds Syntax +public export +record Parameter where + constructor MkParameter + name : WithBounds String + ty : WithBounds Syntax + -- Pretty Print ---------------------------------------------------------------- prettyPrecBounds : Prec -> WithBounds Syntax -> Doc ann @@ -159,3 +165,8 @@ Pretty Definition where pretty def = group $ pretty def.name.val <++> colon <+> softline <+> pretty def.ty.val <+> hardline <+> pretty def.name.val <++> equals <+> softline <+> pretty def.tm.val + +export +Pretty Parameter where + pretty param = group $ + pretty "parameter" <++> pretty param.name.val <++> colon <+> softline <+> pretty param.ty.val |