Render as plain text

Manual/Language/RecursiveDefs/PartialFixpoint.lean

@@ -327,14 +327,6 @@ The tactic solves goals of the form `monotone (fun x => …)` using the followin
 * Zeta-reducing a {keywordOf Lean.Parser.Term.let}`let` expression when value and type do depend on `x`.
 * Applying lemmas annotated with {attr}`partial_fixpoint_monotone`
 
-:::example "List of Monotonicity Lemmas"
-
-::::TODO
-Not really an example, but probably better to have this collapsible?
-::::
-
-The following monotonicity lemmas are registered, and should allow recursive calls in the indicated argument of the higher-order function:
-
 ::::TODO
 
 What I’d like to see here is
@@ -345,6 +337,13 @@ where I use `·` and `_` to distinguish the monotone arguments from others.
 
 ::::
 
+:::example "List of Monotonicity Lemmas"
+
+{TODO}[Not really an example, but probably better to have this collapsible?]
+
+The following monotonicity lemmas are registered, and should allow recursive calls in the indicated argument of the higher-order function:
+
+
 {monotonicityLemmas}
 
 :::

Manual/Meta/Monotonicity.lean

@@ -55,12 +55,11 @@ def monotonicityLemmas : BlockRoleExpander
           let f := concl.appArg!
           unless f.isLambda do
             throwError "Unexpecte conclusion of {name}"
-          lambdaBoundedTelescope f 1 fun _ _call => do
-            -- Could not get this to work:
-            -- let _stx ← Lean.PrettyPrinter.delab call
-            -- `(Inline.code $(quote stx))
-            `(Inline.text "TODO")
-            -- pure (some stx)
+          lambdaBoundedTelescope f 1 fun _ call => do
+            let stx ← Lean.PrettyPrinter.delab call
+            let format := Syntax.prettyPrint stx
+            let str := format.pretty'
+            `(Inline.code $(quote str))
 
       let hl : Highlighted ← constTok name name.toString
       let nameStx ← `(Inline.other {Inline.name with data := ToJson.toJson $(quote hl)} #[Inline.code $(quote name.getString!)])