diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean index 24375f497d..6681c7f5c3 100644 --- a/src/Lean/Elab/PreDefinition/Basic.lean +++ b/src/Lean/Elab/PreDefinition/Basic.lean @@ -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