feat: use |>.

src/Init/Meta.lean

@@ -251,7 +251,7 @@ def mkSepArray (as : Array Syntax) (sep : Syntax) : Array Syntax := do
   let mut r := #[]
   for a in as do
     if i > 0 then
-      r := r.push sep $.push a
+      r := r.push sep |>.push a
     else
       r := r.push a
     i := i + 1

src/Lean/Compiler/BorrowedAnnotation.lean

@@ -11,6 +11,6 @@ def markBorrowed (e : Expr) : Expr :=
 
 @[export lean_is_marked_borrowed]
 def isMarkedBorrowed (e : Expr) : Bool :=
-  annotation? `borrowed e $.isSome
+  annotation? `borrowed e |>.isSome
 
 end Lean

src/Lean/Compiler/ExternAttr.lean

@@ -141,7 +141,7 @@ def getExternEntryFor (d : ExternAttrData) (backend : Name) : Option ExternEntry
   getExternEntryForAux backend d.entries
 
 def isExtern (env : Environment) (fn : Name) : Bool :=
-  getExternAttrData env fn $.isSome
+  getExternAttrData env fn |>.isSome
 
 /- We say a Lean function marked as `[extern "<c_fn_nane>"]` is for all backends, and it is implemented using `extern "C"`.
    Thus, there is no name mangling. -/

src/Lean/Compiler/IR/Borrow.lean

@@ -311,7 +311,7 @@ def collectDecls (decls : Array Decl) : M ParamMap := do
   pure s.paramMap
 
 def infer (env : Environment) (decls : Array Decl) : ParamMap :=
-  collectDecls decls { env := env } $.run' { paramMap := mkInitParamMap env decls }
+  collectDecls decls { env := env } |>.run' { paramMap := mkInitParamMap env decls }
 
 end Borrow
 

src/Lean/Delaborator.lean

@@ -460,9 +460,9 @@ def delabMData : Delab := do
   let pos := (← read).pos
   for (k, v) in m do
     if (`pp).isPrefixOf k then
-      let opts := posOpts.find? pos $.getD {}
+      let opts := posOpts.find? pos |>.getD {}
       posOpts := posOpts.insert pos (opts.insert k v)
-  withReader ({ · with optionsPerPos := posOpts }) $
+  withReader ({ · with optionsPerPos := posOpts }) <|
     withMDataExpr delab
 
 /--

src/Lean/Elab/Declaration.lean

@@ -70,7 +70,7 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
     let type ← mkForallFVars xs type
     let (type, _) ← mkForallUsedOnly vars type
     let (type, _) ← Term.levelMVarToParam type
-    let usedParams  := collectLevelParams {} type $.params
+    let usedParams  := collectLevelParams {} type |>.params
     match sortDeclLevelParams scopeLevelNames allUserLevelNames usedParams with
     | Except.error msg      => throwErrorAt stx msg
     | Except.ok levelParams =>

src/Lean/Elab/Level.lean

@@ -43,14 +43,14 @@ partial def elabLevel (stx : Syntax) : LevelElabM Level := withRef stx do
   if kind == `Lean.Parser.Level.paren then
     elabLevel (stx.getArg 1)
   else if kind == `Lean.Parser.Level.max then
-    let args := stx.getArg 1 $.getArgs
+    let args := stx.getArg 1 |>.getArgs
     let mut lvl ← elabLevel args.back
     for arg in args[:args.size-1] do
       let arg ← elabLevel arg
       lvl := mkLevelMax' lvl arg
     return lvl
   else if kind == `Lean.Parser.Level.imax then
-    let args := stx.getArg 1 $.getArgs
+    let args := stx.getArg 1 |>.getArgs
     let mut lvl ← elabLevel args.back
     for arg in args[:args.size-1] do
       let arg ← elabLevel arg
@@ -69,7 +69,7 @@ partial def elabLevel (stx : Syntax) : LevelElabM Level := withRef stx do
     return mkLevelParam paramName
   else if kind == `Lean.Parser.Level.addLit then
     let lvl ← elabLevel (stx.getArg 0)
-    match stx.getArg 2 $.isNatLit? with
+    match stx.getArg 2 |>.isNatLit? with
     | some val => return lvl.addOffset val
     | none     => throwIllFormedSyntax
   else

src/Lean/Elab/Match.lean

@@ -818,7 +818,7 @@ private def waitExpectedType (expectedType? : Option Expr) : TermElabM Expr := d
 
 private def tryPostponeIfDiscrTypeIsMVar (matchStx : Syntax) : TermElabM Unit := do
   -- We don't wait for the discriminants types when match type is provided by user
-  if getMatchOptType matchStx $.isNone then
+  if getMatchOptType matchStx |>.isNone then
     let discrs := getDiscrs matchStx
     for discr in discrs do
       let term := discr[1]

src/Lean/Elab/PreDefinition/Structural.lean

@@ -382,7 +382,7 @@ partial def addSmartUnfoldingDefAux (preDef : PreDefinition) (matcherBelowDep :
   let isMarkedMatcherName (n : Name) : Bool    := matcherBelowDep.contains n
   let isMarkedMatcherConst (e : Expr) : Bool   := e.isConst && isMarkedMatcherName e.constName!
   let isMarkedMatcherApp (e : Expr) : Bool     := isMarkedMatcherConst e.getAppFn
-  let containsMarkedMatcher (e : Expr) : Bool := e.find? isMarkedMatcherConst $.isSome
+  let containsMarkedMatcher (e : Expr) : Bool := e.find? isMarkedMatcherConst |>.isSome
   let rec visit (e : Expr) : MetaM Expr := do
     match e with
     | Expr.lam ..     => lambdaTelescope e fun xs b => do mkLambdaFVars xs (← visit b)

src/Lean/Elab/Tactic/Basic.lean

@@ -449,7 +449,7 @@ private def findTag? (gs : List MVarId) (tag : Name) : TacticM (Option MVarId) :
 builtin_initialize registerTraceClass `Elab.tactic
 
 @[inline] def TacticM.run {α} (x : TacticM α) (ctx : Context) (s : State) : TermElabM (α × State) :=
-  x ctx $.run s
+  x ctx |>.run s
 
 @[inline] def TacticM.run' {α} (x : TacticM α) (ctx : Context) (s : State) : TermElabM α :=
   Prod.fst <$> x.run ctx s

src/Lean/Elab/Tactic/Induction.lean

@@ -22,7 +22,7 @@ open Meta
   ```
 -/
 private def getAltName (alt : Syntax) : Name :=
-  getNameOfIdent' alt[0] $.eraseMacroScopes
+  getNameOfIdent' alt[0] |>.eraseMacroScopes
 private def getAltVarNames (alt : Syntax) : Array Name :=
   alt[1].getArgs.map getNameOfIdent'
 private def getAltRHS (alt : Syntax) : Syntax :=
@@ -130,7 +130,7 @@ partial def mkElimApp (elimName : Name) (elimInfo : ElimInfo) (targets : Array E
       pure ()
   let f ← Term.mkConst elimName
   let fType ← inferType f
-  let (_, s) ← loop.run { elimInfo := elimInfo, targets := targets } $.run { f := f, fType := fType }
+  let (_, s) ← loop.run { elimInfo := elimInfo, targets := targets } |>.run { f := f, fType := fType }
   Lean.Elab.Term.synthesizeAppInstMVars s.instMVars
   pure { elimApp := (← instantiateMVars s.f), alts := s.alts }
 
@@ -373,7 +373,7 @@ private def getRecInfo (stx : Syntax) (major : Expr) : TacticM RecInfo := withRe
     let (rinfo, _) ← getRecInfoDefault major optInductionAlts false
     pure rinfo
   else
-    let baseRecName := usingRecStx.getIdAt 1 $.eraseMacroScopes
+    let baseRecName := usingRecStx.getIdAt 1 |>.eraseMacroScopes
     let recInfo ← getRecFromUsing major baseRecName
     let recName := recInfo.recursorName
     if optInductionAlts.isNone then

src/Lean/Elab/Tactic/Match.lean

@@ -39,7 +39,7 @@ private def mkAuxiliaryMatchTermAux (parentTag : Name) (matchTac : Syntax) : Sta
   pure result
 
 private def mkAuxiliaryMatchTerm (parentTag : Name) (matchTac : Syntax) : MacroM (Syntax × Array Syntax) := do
-  let (matchTerm, s) ← mkAuxiliaryMatchTermAux parentTag matchTac $.run {}
+  let (matchTerm, s) ← mkAuxiliaryMatchTermAux parentTag matchTac |>.run {}
   pure (matchTerm, s.cases)
 
 @[builtinTactic Lean.Parser.Tactic.match] def evalMatch : Tactic := fun stx => do

src/Lean/Elab/Term.lean

@@ -870,7 +870,7 @@ private def elabUsingElabFnsAux (s : SavedState) (stx : Syntax) (expectedType? :
 
 private def elabUsingElabFns (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone : Bool) : TermElabM Expr := do
   let s ← saveAllState
-  let table := termElabAttribute.ext.getState (← getEnv) $.table
+  let table := termElabAttribute.ext.getState (← getEnv) |>.table
   let k := stx.getKind
   match table.find? k with
   | some elabFns => elabUsingElabFnsAux s stx expectedType? catchExPostpone elabFns
@@ -1244,7 +1244,7 @@ private def mkSomeContext : Context := {
 }
 
 @[inline] def TermElabM.run {α} (x : TermElabM α) (ctx : Context := mkSomeContext) (s : State := {}) : MetaM (α × State) :=
-  withConfig setElabConfig (x ctx $.run s)
+  withConfig setElabConfig (x ctx |>.run s)
 
 @[inline] def TermElabM.run' {α} (x : TermElabM α) (ctx : Context := mkSomeContext) (s : State := {}) : MetaM α :=
   (·.1) <$> x.run ctx s

src/Lean/Hygiene.lean

@@ -87,7 +87,7 @@ private partial def mkFreshInaccessibleUserName (userName : Name) (idx : Nat) :
 
 def sanitizeName (userName : Name) : StateM NameSanitizerState Name := do
   let stem := userName.eraseMacroScopes;
-  let idx  := (← get).nameStem2Idx.find? stem $.getD 0
+  let idx  := (← get).nameStem2Idx.find? stem |>.getD 0
   let san ← mkFreshInaccessibleUserName stem idx
   modify fun s => { s with userName2Sanitized := s.userName2Sanitized.insert userName san }
   pure san

src/Lean/Meta/AbstractNestedProofs.lean

@@ -63,6 +63,6 @@ end AbstractNestedProofs
 
 /-- Replace proofs nested in `e` with new lemmas. The new lemmas have names of the form `mainDeclName.proof_<idx>` -/
 def abstractNestedProofs (mainDeclName : Name) (e : Expr) : MetaM Expr :=
-  AbstractNestedProofs.visit e $.run { baseName := mainDeclName } $.run $.run' { nextIdx := 1 }
+  AbstractNestedProofs.visit e |>.run { baseName := mainDeclName } |>.run |>.run' { nextIdx := 1 }
 
 end Lean.Meta

src/Lean/Meta/Basic.lean

@@ -131,7 +131,7 @@ instance : AddMessageContext MetaM := {
 }
 
 @[inline] def MetaM.run {α} (x : MetaM α) (ctx : Context := {}) (s : State := {}) : CoreM (α × State) :=
-  x ctx $.run s
+  x ctx |>.run s
 
 @[inline] def MetaM.run' {α} (x : MetaM α) (ctx : Context := {}) (s : State := {}) : CoreM α :=
   Prod.fst <$> x.run ctx s

src/Lean/Meta/ExprDefEq.lean

@@ -573,7 +573,7 @@ partial def check (e : Expr) : CheckAssignmentM Expr := do
     catchInternalIds [outOfScopeExceptionId, checkAssignmentExceptionId]
       (do let e ← x; pure $ some e)
       (fun _ => pure none)
-  x.run ctx $.run' {}
+  x.run ctx |>.run' {}
 
 end CheckAssignment
 

src/Lean/Meta/ForEachExpr.lean

@@ -51,7 +51,7 @@ end
 end ForEachExpr
 
 def forEachExprImp' (e : Expr) (f : Expr → MetaM Bool) : MetaM Unit :=
-  ForEachExpr.visit f e $.run
+  ForEachExpr.visit f e |>.run
 
 /-- Similar to `Expr.forEach'`, but creates free variables whenever going inside of a binder. -/
 def forEachExpr' {m} [MonadLiftT MetaM m] (e : Expr) (f : Expr → MetaM Bool) : m Unit :=

src/Lean/Meta/InferType.lean

@@ -157,7 +157,7 @@ private def isAlwaysZero : Level → Bool
    if `type` is of the form `A_1 -> ... -> A_n -> Prop`.
    Remark: `type` can be a dependent arrow. -/
 private partial def isArrowProp : Expr → Nat → MetaM LBool
-  | Expr.sort u _,        0   => return isAlwaysZero (← instantiateLevelMVars u) $.toLBool
+  | Expr.sort u _,        0   => return isAlwaysZero (← instantiateLevelMVars u) |>.toLBool
   | Expr.forallE _ _ _ _, 0   => pure LBool.false
   | Expr.forallE _ _ b _, n+1 => isArrowProp b n
   | Expr.letE _ _ _ b _,  n   => isArrowProp b n

src/Lean/Meta/Match/Match.lean

@@ -476,7 +476,7 @@ end Unify
 private def unify? (altFVarDecls : List LocalDecl) (a b : Expr) : MetaM (Option FVarSubst) := do
   let a ← instantiateMVars a
     let b ← instantiateMVars b
-    let (b, s) ← Unify.unify a b { altFVarDecls := altFVarDecls} $.run {}
+    let (b, s) ← Unify.unify a b { altFVarDecls := altFVarDecls} |>.run {}
     if b then pure s.fvarSubst else pure none
 
 private def expandVarIntoCtor? (alt : Alt) (fvarId : FVarId) (ctorName : Name) : MetaM (Option Alt) :=

src/Lean/Meta/SynthInstance.lean

@@ -128,7 +128,7 @@ end MkTableKey
 
 /- Remark: `mkTableKey` assumes `e` does not contain assigned metavariables. -/
 def mkTableKey (mctx : MetavarContext) (e : Expr) : Expr :=
-  MkTableKey.normExpr e mctx $.run' {}
+  MkTableKey.normExpr e mctx |>.run' {}
 
 structure Answer :=
   (result     : AbstractMVarsResult)

src/Lean/Meta/Transform.lean

@@ -49,7 +49,7 @@ partial def transform {m} [Monad m] [MonadLiftT CoreM m] [MonadControlT CoreM m]
         | Expr.mdata _ b _     => visitPost (e.updateMData! (← visit b))
         | Expr.proj _ _ b _    => visitPost (e.updateProj! (← visit b))
         | _                    => visitPost e
-  visit input $.run
+  visit input |>.run
 
 end Core
 
@@ -102,7 +102,7 @@ partial def transform {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m]
         | Expr.mdata _ b _   => visitPost (e.updateMData! (← visit b))
         | Expr.proj _ _ b _  => visitPost (e.updateProj! (← visit b))
         | _                  => visitPost e
-  visit input $.run
+  visit input |>.run
 
 end Meta
 end Lean

src/Lean/MetavarContext.lean

@@ -594,7 +594,7 @@ def instantiateMVars (mctx : MetavarContext) (e : Expr) : Expr × MetavarContext
   else
     let instantiate {ω} (e : Expr) : (MonadCacheT Expr Expr $ StateRefT MetavarContext $ ST ω) Expr :=
       instantiateExprMVars e
-    runST fun _ => instantiate e $.run $.run mctx
+    runST fun _ => instantiate e |>.run |>.run mctx
 
 def instantiateLCtxMVars (mctx : MetavarContext) (lctx : LocalContext) : LocalContext × MetavarContext :=
   lctx.foldl

src/Lean/ParserCompiler.lean

@@ -134,7 +134,7 @@ unsafe def registerParserCompiler {α} (ctx : Context α) : IO Unit := do
       if info.type.isConstOf `Lean.ParserDescr || info.type.isConstOf `Lean.TrailingParserDescr then
         let d ← evalConstCheck ParserDescr `Lean.ParserDescr constName <|>
           evalConstCheck TrailingParserDescr `Lean.TrailingParserDescr constName
-        compileEmbeddedParsers ctx d $.run'
+        compileEmbeddedParsers ctx d |>.run'
       else
         if catName.isAnonymous then
           -- `[runBuiltinParserAttributeHooks]` => force compilation even if imported, do not apply `ctx.categoryAttr`.

src/Lean/ResolveName.lean

@@ -25,7 +25,7 @@ builtin_initialize aliasExtension : SimplePersistentEnvExtension AliasEntry Alia
   registerSimplePersistentEnvExtension {
     name          := `aliasesExt,
     addEntryFn    := addAliasEntry,
-    addImportedFn := fun es => mkStateFromImportedEntries addAliasEntry {} es $.switch
+    addImportedFn := fun es => mkStateFromImportedEntries addAliasEntry {} es |>.switch
   }
 
 /- Add alias `a` for `e` -/
@@ -33,7 +33,7 @@ builtin_initialize aliasExtension : SimplePersistentEnvExtension AliasEntry Alia
   aliasExtension.addEntry env (a, e)
 
 def getAliases (env : Environment) (a : Name) : List Name :=
-  match aliasExtension.getState env $.find? a with
+  match aliasExtension.getState env |>.find? a with
   | none    => []
   | some es => es
 

src/Lean/Util/PPExt.lean

@@ -43,7 +43,7 @@ builtin_initialize ppExt : EnvExtension PPFns ←
   registerEnvExtension $ ppFnsRef.get
 
 def ppExpr (ctx : PPContext) (e : Expr) : IO Format :=
-  let e := ctx.mctx.instantiateMVars e $.1
+  let e := ctx.mctx.instantiateMVars e |>.1
   if getPPRaw ctx.opts then
     pure $ format (toString e)
   else

src/Lean/Util/PPGoal.lean

@@ -26,7 +26,7 @@ def ppGoal (ppCtx : PPContext) (mvarId : MVarId) : IO Format :=
     let lctx         := lctx.sanitizeNames.run' { options := opts }
     let ppCtx        := { ppCtx with lctx := lctx }
     let pp (e : Expr) : IO Format := ppExpr ppCtx e
-    let instMVars (e : Expr) : Expr := mctx.instantiateMVars e $.1
+    let instMVars (e : Expr) : Expr := mctx.instantiateMVars e |>.1
     let addLine (fmt : Format) : Format := if fmt.isNil then fmt else fmt ++ Format.line
     -- The followint two `let rec`s are being used to control the generated code size.
     -- Then should be remove after we rewrite the compiler in Lean

src/Lean/Util/Recognizers.lean

@@ -86,7 +86,7 @@ def isConstructorApp? (env : Environment) (e : Expr) : Option ConstructorVal :=
     | _ => none
 
 def isConstructorApp (env : Environment) (e : Expr) : Bool :=
-  e.isConstructorApp? env $.isSome
+  e.isConstructorApp? env |>.isSome
 
 def constructorApp? (env : Environment) (e : Expr) : Option (ConstructorVal × Array Expr) :=
   match e with