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

chore: use doc string

Browse source
This commit is contained in:
Leonardo de Moura 2021-09-17 11:53:12 -07:00
parent dc32a827b3
commit 94ede53940
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Elab/PreDefinition/Basic.lean
View file

@ -13,9 +13,9 @@ namespace Lean.Elab
open Meta
open Term
/-
A (potentially recursive) definition.
The elaborator converts it into Kernel definitions using many different strategies.
/--
A (potentially recursive) definition.
The elaborator converts it into Kernel definitions using many different strategies.
-/
structure PreDefinition where
ref : Syntax