fix: indentation issues

This commit is contained in:
Leonardo de Moura 2021-03-12 10:57:07 -08:00
parent a683aee360
commit 472c5fb900
3 changed files with 8 additions and 8 deletions

View file

@ -204,8 +204,7 @@ instance : Repr Substring where
reprPrec s _ := Format.text <| String.quote s.toString ++ ".toSubstring"
instance : Repr String.Iterator where
reprPrec | ⟨s, pos⟩, prec =>
Repr.addAppParen ("String.Iterator.mk " ++ reprArg s ++ " " ++ reprArg pos) prec
reprPrec | ⟨s, pos⟩, prec => Repr.addAppParen ("String.Iterator.mk " ++ reprArg s ++ " " ++ reprArg pos) prec
instance (n : Nat) : Repr (Fin n) where
reprPrec f _ := repr f.val

View file

@ -77,12 +77,13 @@ instance : ToStream Std.Range Std.Range where
toStream r := r
instance [Stream ρ α] [Stream γ β] : Stream (ρ × γ) (α × β) where
next? | (s₁, s₂) =>
match Stream.next? s₁ with
| none => none
| some (a, s₁) => match Stream.next? s₂ with
next?
| (s₁, s₂) =>
match Stream.next? s₁ with
| none => none
| some (b, s₂) => some ((a, b), (s₁, s₂))
| some (a, s₁) => match Stream.next? s₂ with
| none => none
| some (b, s₂) => some ((a, b), (s₁, s₂))
instance : Stream (List α) α where
next?

View file

@ -953,7 +953,7 @@ private def isLambdaWithImplicit (stx : Syntax) : Bool :=
| `(fun $binders* => $body) => binders.any fun b => b.isOfKind `Lean.Parser.Term.implicitBinder || b.isOfKind `Lean.Parser.Term.instBinder
| _ => false
private partial def dropTermParens : Syntax → Syntax | stx =>
private partial def dropTermParens : Syntax → Syntax := fun stx =>
match stx with
| `(($stx)) => dropTermParens stx
| _ => stx