max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: heading (#2180)

Browse source 
Add '#' to the docstring.
This commit is contained in:
Bulhwi Cha 2023-04-03 16:40:22 +09:00 • committed by GitHub
parent 6d583284df
commit d694bf2d09
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Prelude.lean
View file

@ -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