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

chore: indent syntax

Browse source
This commit is contained in:
Leonardo de Moura 2021-03-31 14:28:35 -07:00
parent 7c2338546c
commit 583afaab10
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Elab/DeclModifiers.lean
View file

@ -76,7 +76,7 @@ def expandOptDocComment? [Monad m] [MonadError m] (optDocComment : Syntax) : m (
| none => pure none
| some s => match s[1] with
| Syntax.atom _ val => pure (some (val.extract 0 (val.bsize - 2)))
| _ => throwErrorAt s "unexpected doc string {s[1]}"
| _ => throwErrorAt s "unexpected doc string{indentD s[1]}"
section Methods
@ -93,7 +93,7 @@ def elabModifiers (stx : Syntax) : m Modifiers := do
| none => pure none
| some s => match s[1] with
| Syntax.atom _ val => pure (some (val.extract 0 (val.bsize - 2)))
| _ => throwErrorAt s "unexpected doc string {s[1]}"
| _ => throwErrorAt s "unexpected doc string{indentD s[1]}"
let visibility ← match visibilityStx.getOptional? with
| none => pure Visibility.regular
| some v =>