Use ppExpr

leanprover · Jan 20, 2025 · 8478f38 · 8478f38
1 parent 39f81f1
commit 8478f38
Showing 1 changed file with 2 additions and 4 deletions.
diff --git a/Manual/Meta/Monotonicity.lean b/Manual/Meta/Monotonicity.lean
@@ -96,10 +96,8 @@ def monotonicityLemmas : BlockRoleExpander
               else
                 pure .continue)
 
-            let stx ← Lean.PrettyPrinter.delab call'
-            let fmt ← Lean.PrettyPrinter.formatTerm stx
-            let str : String := fmt.pretty
-            `(Inline.code $(quote str))
+            let fmt ← ppExpr call'
+            `(Inline.code $(quote fmt.pretty))
 
       pure #[nameStx, patternStx]