From 9ee3cb642a4ca586fa876e103e64c95bd01bb1db Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 2 Apr 2022 07:53:12 -0700
Subject: [PATCH] chore: formatting

---
 doc/examples/bintree.lean | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/doc/examples/bintree.lean b/doc/examples/bintree.lean
index 46c09e333d..37622c710e 100644
--- a/doc/examples/bintree.lean
+++ b/doc/examples/bintree.lean
@@ -105,10 +105,11 @@ The proof of the auxiliary theorem is by induction on `t`\ .
 The `generalizing acc` modifier instructs Lean to revert `acc`\ , apply the
 induction theorem for `Tree`\ s, and then reintroduce `acc` in each case.
 By using `generalizing`\ , we obtain the more general induction hypotheses
-```lean
-left_ih : ∀ acc, toListTR.go left acc = toList left ++ acc
-right_ih : ∀ acc, toListTR.go right acc = toList right ++ acc
-```
+
+- `left_ih : ∀ acc, toListTR.go left acc = toList left ++ acc`
+
+- `right_ih : ∀ acc, toListTR.go right acc = toList right ++ acc`
+
 Recall that the combinator `tac <;> tac'` runs `tac` on the main goal and `tac'` on each produced goal,
 concatenating all goals produced by `tac'`\ . In this theorem, we use it to apply
 `simp` and close each subgoal produced by the `induction` tactic.