Skip to content

Commit

Permalink
extraneous whitespace
Browse files Browse the repository at this point in the history
  • Loading branch information
kmill committed Nov 21, 2024
1 parent d65ac82 commit c9a9d90
Showing 1 changed file with 1 addition and 3 deletions.
4 changes: 1 addition & 3 deletions src/Lean/Elab/StructInst.lean
Original file line number Diff line number Diff line change
Expand Up @@ -178,8 +178,6 @@ where
let r ← go sources (sourcesNew.push sourceNew)
`(let __src := $source; $r)



/--
An *explicit source* is one of the structures `sᵢ` that appear in `{ s₁, …, sₙ with … }`.
-/
Expand Down Expand Up @@ -244,7 +242,7 @@ private def isModifyOp? (stx : Syntax) : TermElabM (Option Syntax) := do
let s? ← stx[2][0].getSepArgs.foldlM (init := none) fun s? arg => do
/- arg is of the form `structInstField` -/
if arg.getKind == ``Lean.Parser.Term.structInstField then
/- Remark: the syntax for `structInstField` (after expansion) is
/- Remark: the syntax for `structInstField` after macro expansion is
```
def structInstLVal := leading_parser (ident <|> numLit <|> structInstArrayRef) >> many (group ("." >> (ident <|> numLit)) <|> structInstArrayRef)
def structInstField := leading_parser
Expand Down

0 comments on commit c9a9d90

Please sign in to comment.