From f67c93191fded3e469f627998ba237b6262dc717 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 19 Nov 2020 08:38:47 -0800 Subject: [PATCH] feat: use `|>.` --- src/Init/Meta.lean | 2 +- src/Lean/Compiler/BorrowedAnnotation.lean | 2 +- src/Lean/Compiler/ExternAttr.lean | 2 +- src/Lean/Compiler/IR/Borrow.lean | 2 +- src/Lean/Delaborator.lean | 4 ++-- src/Lean/Elab/Declaration.lean | 2 +- src/Lean/Elab/Level.lean | 6 +++--- src/Lean/Elab/Match.lean | 2 +- src/Lean/Elab/PreDefinition/Structural.lean | 2 +- src/Lean/Elab/Tactic/Basic.lean | 2 +- src/Lean/Elab/Tactic/Induction.lean | 6 +++--- src/Lean/Elab/Tactic/Match.lean | 2 +- src/Lean/Elab/Term.lean | 4 ++-- src/Lean/Hygiene.lean | 2 +- src/Lean/Meta/AbstractNestedProofs.lean | 2 +- src/Lean/Meta/Basic.lean | 2 +- src/Lean/Meta/ExprDefEq.lean | 2 +- src/Lean/Meta/ForEachExpr.lean | 2 +- src/Lean/Meta/InferType.lean | 2 +- src/Lean/Meta/Match/Match.lean | 2 +- src/Lean/Meta/SynthInstance.lean | 2 +- src/Lean/Meta/Transform.lean | 4 ++-- src/Lean/MetavarContext.lean | 2 +- src/Lean/ParserCompiler.lean | 2 +- src/Lean/ResolveName.lean | 4 ++-- src/Lean/Util/PPExt.lean | 2 +- src/Lean/Util/PPGoal.lean | 2 +- src/Lean/Util/Recognizers.lean | 2 +- 28 files changed, 36 insertions(+), 36 deletions(-) diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index 1670ed91a8..df6d5fe1dd 100644 --- a/src/Init/Meta.lean +++ b/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 diff --git a/src/Lean/Compiler/BorrowedAnnotation.lean b/src/Lean/Compiler/BorrowedAnnotation.lean index f606f8d90c..4800e18125 100644 --- a/src/Lean/Compiler/BorrowedAnnotation.lean +++ b/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 diff --git a/src/Lean/Compiler/ExternAttr.lean b/src/Lean/Compiler/ExternAttr.lean index c73342b402..e053a1bf18 100644 --- a/src/Lean/Compiler/ExternAttr.lean +++ b/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 ""]` is for all backends, and it is implemented using `extern "C"`. Thus, there is no name mangling. -/ diff --git a/src/Lean/Compiler/IR/Borrow.lean b/src/Lean/Compiler/IR/Borrow.lean index a2f3a1fff2..c8cb2dcec7 100644 --- a/src/Lean/Compiler/IR/Borrow.lean +++ b/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 diff --git a/src/Lean/Delaborator.lean b/src/Lean/Delaborator.lean index 458c83f00b..24bdd9fe7e 100644 --- a/src/Lean/Delaborator.lean +++ b/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 /-- diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean index 261cab3a2e..a841af3278 100644 --- a/src/Lean/Elab/Declaration.lean +++ b/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 => diff --git a/src/Lean/Elab/Level.lean b/src/Lean/Elab/Level.lean index 1527e06d18..f3413ef504 100644 --- a/src/Lean/Elab/Level.lean +++ b/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 diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index 35c6def848..da703be981 100644 --- a/src/Lean/Elab/Match.lean +++ b/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] diff --git a/src/Lean/Elab/PreDefinition/Structural.lean b/src/Lean/Elab/PreDefinition/Structural.lean index b24708e267..e5320a851c 100644 --- a/src/Lean/Elab/PreDefinition/Structural.lean +++ b/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) diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index e78248f122..2695cc30fa 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ 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 diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index 7d03636afd..5163585b26 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/Match.lean b/src/Lean/Elab/Tactic/Match.lean index e93cecbae9..2d856a4b6e 100644 --- a/src/Lean/Elab/Tactic/Match.lean +++ b/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 diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 05d3389b3b..bb6fe14269 100644 --- a/src/Lean/Elab/Term.lean +++ b/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 diff --git a/src/Lean/Hygiene.lean b/src/Lean/Hygiene.lean index 2e12950ab9..2a6964a531 100644 --- a/src/Lean/Hygiene.lean +++ b/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 diff --git a/src/Lean/Meta/AbstractNestedProofs.lean b/src/Lean/Meta/AbstractNestedProofs.lean index 31df038786..0a42c6fcbd 100644 --- a/src/Lean/Meta/AbstractNestedProofs.lean +++ b/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_` -/ 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 diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 22ef4c9fa2..5df21ef3b1 100644 --- a/src/Lean/Meta/Basic.lean +++ b/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 diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index cc3f6ed03f..403ebb2a59 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/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 diff --git a/src/Lean/Meta/ForEachExpr.lean b/src/Lean/Meta/ForEachExpr.lean index b972155116..743436e8f2 100644 --- a/src/Lean/Meta/ForEachExpr.lean +++ b/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 := diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean index e2239016d8..b7a0e8a388 100644 --- a/src/Lean/Meta/InferType.lean +++ b/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 diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index 674fc723f0..94818a01c1 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/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) := diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index b6c6629921..e7f5aafec0 100644 --- a/src/Lean/Meta/SynthInstance.lean +++ b/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) diff --git a/src/Lean/Meta/Transform.lean b/src/Lean/Meta/Transform.lean index 348ef08f22..755f197b75 100644 --- a/src/Lean/Meta/Transform.lean +++ b/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 diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index b0f48e5c99..74346a1eca 100644 --- a/src/Lean/MetavarContext.lean +++ b/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 diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean index 7364637ff5..459c4987d8 100644 --- a/src/Lean/ParserCompiler.lean +++ b/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`. diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean index 44920a05f7..874493db79 100644 --- a/src/Lean/ResolveName.lean +++ b/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 diff --git a/src/Lean/Util/PPExt.lean b/src/Lean/Util/PPExt.lean index 1a59548073..391f9919cb 100644 --- a/src/Lean/Util/PPExt.lean +++ b/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 diff --git a/src/Lean/Util/PPGoal.lean b/src/Lean/Util/PPGoal.lean index af56624a3c..61acec3c14 100644 --- a/src/Lean/Util/PPGoal.lean +++ b/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 diff --git a/src/Lean/Util/Recognizers.lean b/src/Lean/Util/Recognizers.lean index e1e8aa3605..00ef8236e8 100644 --- a/src/Lean/Util/Recognizers.lean +++ b/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