From 0fdd4741be7850577f184cdf2535d4f5381b1a9b Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Thu, 7 Dec 2023 01:37:08 +0100 Subject: [PATCH] print quantity on let --- lib/Quox/Syntax/Term/Pretty.idr | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr index e686a74..e51513d 100644 --- a/lib/Quox/Syntax/Term/Pretty.idr +++ b/lib/Quox/Syntax/Term/Pretty.idr @@ -349,9 +349,10 @@ prettyLets dnames xs lets = sequence $ snd $ go lets where go (lets :< (qty, x, rhs)) = let (ys, docs) = go lets doc = do - x <- prettyTBind x - rhs <- withPrec Outer $ assert_total prettyElim dnames ys rhs - hangDSingle (hsep [!letD, x, !cstD]) (hsep [rhs, !inD]) in + lett <- [|letD <+> prettyQty qty|] + x <- prettyTBind x + rhs <- withPrec Outer $ assert_total prettyElim dnames ys rhs + hangDSingle (hsep [lett, x, !cstD]) (hsep [rhs, !inD]) in (ys :< x, docs :< doc)