From 0ecd9e608ced18f70f465c986d6519e8e95b0b6b Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Wed, 20 Nov 2024 15:31:25 +0000 Subject: Improve syntactic sugar. Sugar makes programs nicer to write. --- src/Inky/Term/Pretty/Error.idr | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/Inky/Term/Pretty/Error.idr') 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 -- cgit v1.2.3