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)