From 9333fb4cf66215677f555fed62b1892f0d6ff32f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 12 Dec 2020 08:34:00 -0800 Subject: [PATCH] chore: style --- src/Init/Prelude.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index e17247cbbf..8290fe254e 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -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