diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2024-11-20 15:31:25 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2024-11-20 15:31:25 +0000 |
| commit | 0ecd9e608ced18f70f465c986d6519e8e95b0b6b (patch) | |
| tree | 32214f9e93eecbb6b1cc4aea12af1eba93f19ab7 /src/Inky/Term/Pretty | |
| parent | 3f72d28b7b348d441dde0e66e848ed4d7c16f5ba (diff) | |
Improve syntactic sugar.
Sugar makes programs nicer to write.
Diffstat (limited to 'src/Inky/Term/Pretty')
| -rw-r--r-- | src/Inky/Term/Pretty/Error.idr | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Inky/Term/Pretty/Error.idr b/src/Inky/Term/Pretty/Error.idr index a5ee2fa..d87178f 100644 --- a/src/Inky/Term/Pretty/Error.idr +++ b/src/Inky/Term/Pretty/Error.idr @@ -22,6 +22,7 @@ Pretty (ChecksOnly t) where pretty Roll = "rolling" pretty Fold = "fold" +export prettyNotSynths : {tyCtx, tmCtx : SnocList String} -> {e : Term mode m tyCtx tmCtx} -> @@ -99,7 +100,7 @@ prettyNotSynths (PrjNS2 prf f) = , pretty "cannot project non-product type" <+> line <+> prettyType a Open )] -prettyNotSynths (PrjNS3 {l, as} prf contra) = +prettyNotSynths (PrjNS3 {l, e, as} prf contra) = case synthsRecompute prf of Val (TProd as) => [(e.meta |