From 0a5df7cd6dd3501c8a17c2dca7c842b3053ae231 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 5 Jul 2022 15:21:33 -0700 Subject: [PATCH] chore: style --- src/Std/Data/PersistentArray.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Std/Data/PersistentArray.lean b/src/Std/Data/PersistentArray.lean index e19d044060..367652b66d 100644 --- a/src/Std/Data/PersistentArray.lean +++ b/src/Std/Data/PersistentArray.lean @@ -71,7 +71,7 @@ partial def setAux : PersistentArrayNode α → USize → USize → α → Persi let j := div2Shift i shift let i := mod2Shift i shift let shift := shift - initShift - node $ cs.modify j.toNat $ fun c => setAux c i shift a + node <| cs.modify j.toNat fun c => setAux c i shift a | leaf cs, i, _, a => leaf (cs.set! i.toNat a) def set (t : PersistentArray α) (i : Nat) (a : α) : PersistentArray α := @@ -85,7 +85,7 @@ def set (t : PersistentArray α) (i : Nat) (a : α) : PersistentArray α := let j := div2Shift i shift let i := mod2Shift i shift let shift := shift - initShift - node $ cs.modify j.toNat $ fun c => modifyAux f c i shift + node <| cs.modify j.toNat fun c => modifyAux f c i shift | leaf cs, i, _ => leaf (cs.modify i.toNat f) @[specialize] def modify [Inhabited α] (t : PersistentArray α) (i : Nat) (f : α → α) : PersistentArray α := @@ -109,9 +109,9 @@ partial def insertNewLeaf : PersistentArrayNode α → USize → USize → Array let i := mod2Shift i shift let shift := shift - initShift if j.toNat < cs.size then - node $ cs.modify j.toNat fun c => insertNewLeaf c i shift a + node <| cs.modify j.toNat fun c => insertNewLeaf c i shift a else - node $ cs.push $ mkNewPath shift a + node <| cs.push <| mkNewPath shift a | n, _, _, _ => n -- unreachable def mkNewTail (t : PersistentArray α) : PersistentArray α :=