From 7f00352d332d79e8a991388ad15e5d79dd7ddeaa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 2 Apr 2022 06:55:23 -0700 Subject: [PATCH] chore: backtick issue in documentation --- doc/examples/bintree.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/examples/bintree.lean b/doc/examples/bintree.lean index 2faa4a6a07..85b3d4619a 100644 --- a/doc/examples/bintree.lean +++ b/doc/examples/bintree.lean @@ -169,7 +169,7 @@ theorem Tree.bst_insert_of_bst {t : Tree β} (h : BST t) (key : Nat) (value : β exact .node h₁ h₂ b₁ b₂ /-| -Now, we define the type `BinTree` using a `Subtype` that states that only trees satisfying the BST invariant are `BinTree`s. +Now, we define the type `BinTree` using a `Subtype` that states that only trees satisfying the BST invariant are `BinTree`\ s. -/ def BinTree (β : Type u) := { t : Tree β // BST t }