From d694bf2d09b86d6ec3f218ed03e70b6e9672f5d2 Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Mon, 3 Apr 2023 16:40:22 +0900 Subject: [PATCH] doc: heading (#2180) Add '#' to the docstring. --- src/Init/Prelude.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 29c4a59560..3afdc97d05 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -3656,7 +3656,7 @@ instance : Inhabited Syntax where instance : Inhabited (TSyntax ks) where default := ⟨default⟩ -/-! Builtin kinds -/ +/-! # Builtin kinds -/ /-- The `choice` kind is used when a piece of syntax has multiple parses, and the