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

chore: style

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-12 08:34:00 -08:00
parent bb8cd95437
commit 9333fb4cf6
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/Init/Prelude.lean
View file

@ -1692,8 +1692,8 @@ def getPos (stx : Syntax) : Option String.Pos :=
/--
An array of syntax elements interspersed with separators. Can be coerced to/from `Array Syntax` to automatically
remove/insert the separators. -/
structure SepArray (sep : String) :=
(elemsAndSeps : Array Syntax)
structure SepArray (sep : String) where
elemsAndSeps : Array Syntax
end Syntax