chore: update stage0

stage0/src/Init/Control/Monad.lean

@@ -15,7 +15,7 @@ class HasBind (m : Type u → Type v) :=
 
 export HasBind (bind)
 
-infixr `>>=` := bind
+infixl `>>=` := bind
 
 @[inline] def mcomp {α : Type u} {β δ : Type v} {m : Type v → Type w} [HasBind m] (f : α → m β) (g : β → m δ) : α → m δ :=
 fun a => f a >>= g

stage0/src/Init/Core.lean

@@ -66,7 +66,7 @@ reserve infixr ` :: `:67
 
 /- Control -/
 reserve infixr ` <|> `:2
-reserve infixr ` >>= `:55
+reserve infixl ` >>= `:55
 reserve infixr ` >=> `:55
 reserve infixl ` <*> `:60
 reserve infixl ` <* ` :60

stage0/src/Lean/Elab/Term.lean

@@ -996,9 +996,10 @@ opts ← getOptions;
 mctx ← getMCtx;
 lctx ← getLCtx;
 match Lean.mkAuxDefinition env opts mctx lctx declName type value zeta with
-| Except.error ex    => throwError ref (ex.toMessageData opts)
-| Except.ok (r, env) => do
+| Except.error ex          => throwError ref (ex.toMessageData opts)
+| Except.ok (r, env, mctx) => do
   setEnv env;
+  setMCtx mctx;
   pure r
 
 private partial def mkAuxNameAux (env : Environment) (base : Name) : Nat → Name

stage0/src/Lean/Expr.lean

@@ -638,8 +638,8 @@ constant abstractRange (e : @& Expr) (n : @& Nat) (xs : @& Array Expr) : Expr :=
 def replaceFVar (e : Expr) (fvar : Expr) (v : Expr) : Expr :=
 (e.abstract #[fvar]).instantiate1 v
 
-def replaceFVarId (e : Expr) (fvarId : FVarId) (v : Expr) : Expr :=
-replaceFVar e (mkFVar fvarId) v
+def replaceFVarId (e : Expr) (fvarId : FVarId) (newFVarId : FVarId) : Expr :=
+replaceFVar e (mkFVar fvarId) (mkFVar newFVarId)
 
 instance : HasToString Expr :=
 ⟨Expr.dbgToString⟩

stage0/src/Lean/Meta/Basic.lean

@@ -110,6 +110,7 @@ structure Cache :=
 (funInfo       : PersistentHashMap InfoCacheKey FunInfo := {})
 (synthInstance : PersistentHashMap Expr (Option Expr) := {})
 (whnfDefault   : PersistentExprStructMap Expr := {}) -- cache for closed terms and `TransparencyMode.default`
+(whnfAll       : PersistentExprStructMap Expr := {}) -- cache for closed terms and `TransparencyMode.all`
 
 structure Context :=
 (config         : Config         := {})
@@ -152,10 +153,13 @@ ctx ← read; pure ctx.config
 @[inline] def getMCtx : MetaM MetavarContext := do
 s ← get; pure s.mctx
 
+def setMCtx (mctx : MetavarContext) : MetaM Unit := do
+modify $ fun s => { s with mctx := mctx }
+
 @[inline] def getEnv : MetaM Environment := do
 s ← get; pure s.env
 
-@[inline] def setEnv (env : Environment) : MetaM Unit := do
+def setEnv (env : Environment) : MetaM Unit := do
 modify $ fun s => { s with env := env }
 
 def mkWHNFRef : IO (IO.Ref (Expr → MetaM Expr)) :=
@@ -250,6 +254,11 @@ ctx ← read;
 s ← get;
 throw (f { env := s.env, mctx := s.mctx, lctx := ctx.lctx, opts := ctx.config.opts })
 
+def throwOther {α} (msg : MessageData) : MetaM α := do
+ctx ← read;
+s ← get;
+throw (Exception.other (MessageData.withContext { env := s.env, mctx := s.mctx, lctx := ctx.lctx, opts := ctx.config.opts } msg))
+
 def throwBug {α} (b : Bug) : MetaM α :=
 throwEx $ Exception.bug b
 
@@ -837,13 +846,13 @@ finally x (modify $ fun s => { s with mctx := mctx' })
   returned where `u_i`s are universe parameters and metavariables `type` and `value` depend on,
   and `t_j`s are free and meta variables `type` and `value` depend on. -/
 def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM Expr := do
-env  ← getEnv;
-opts ← getOptions;
-mctx ← getMCtx;
-lctx ← getLCtx;
+env   ← getEnv;
+opts  ← getOptions;
+mctx  ← getMCtx;
+lctx  ← getLCtx;
 match Lean.mkAuxDefinition env opts mctx lctx name type value with
-| Except.error ex    => throw $ Exception.kernel ex opts
-| Except.ok (e, env) => do setEnv env; pure e
+| Except.error ex          => throw $ Exception.kernel ex opts
+| Except.ok (e, env, mctx) => do setEnv env; setMCtx mctx; pure e
 
 /-- Similar to `mkAuxDefinition`, but infers the type of `value`. -/
 def mkAuxDefinitionFor (name : Name) (value : Expr) : MetaM Expr := do

stage0/src/Lean/Meta/Tactic/Cases.lean

@@ -174,10 +174,10 @@ s.mapIdx $ fun i s => { ctorName := ctorNames.get! i, toInductionSubgoal := s }
 
 private partial def unifyEqsAux : Nat → CasesSubgoal → MetaM (Option CasesSubgoal)
 | 0,   s => do
-  trace! `Meta.cases ("unifyEqs " ++ MessageData.ofGoal s.mvarId);
+  trace! `Meta.Tactic.cases ("unifyEqs " ++ MessageData.ofGoal s.mvarId);
   pure (some s)
 | n+1, s => do
-  trace! `Meta.cases ("unifyEqs [" ++ toString (n+1) ++ "] " ++ MessageData.ofGoal s.mvarId);
+  trace! `Meta.Tactic.cases ("unifyEqs [" ++ toString (n+1) ++ "] " ++ MessageData.ofGoal s.mvarId);
   (eqFVarId, mvarId) ← intro1 s.mvarId;
   withMVarContext mvarId $ do
     eqDecl ← getLocalDecl eqFVarId;
@@ -243,7 +243,7 @@ withMVarContext mvarId $ do
         pure $ toCasesSubgoals s ctors)
       (do
         s₁ ← generalizeIndices mvarId majorFVarId;
-        trace! `Meta.cases ("after generalizeIndices" ++ Format.line ++ MessageData.ofGoal s₁.mvarId);
+        trace! `Meta.Tactic.cases ("after generalizeIndices" ++ Format.line ++ MessageData.ofGoal s₁.mvarId);
         s₂ ← induction s₁.mvarId s₁.fvarId casesOn givenNames useUnusedNames;
         s₂ ← elimAuxIndices s₁ s₂;
         let s₂ := toCasesSubgoals s₂ ctors;
@@ -254,5 +254,8 @@ end Cases
 def cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array (List Name) := #[]) (useUnusedNames := false) : MetaM (Array CasesSubgoal) :=
 Cases.cases mvarId majorFVarId givenNames useUnusedNames
 
+@[init] private def regTraceClasses : IO Unit := do
+registerTraceClass `Meta.Tactic.cases
+
 end Meta
 end Lean

stage0/src/Lean/Meta/Tactic/FVarSubst.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Expr
+import Lean.LocalContext
 import Lean.Util.ReplaceExpr
 
 namespace Lean
@@ -62,6 +63,17 @@ else oldS.map.fold
       | some fvarId'' => m.insert fvarId fvarId'')
   newS
 
+def domain (s : FVarSubst) : List FVarId :=
+s.map.fold (fun r k v => k :: r) []
+
 end FVarSubst
 end Meta
+
+def LocalDecl.applyFVarSubst (s : Meta.FVarSubst) : LocalDecl → LocalDecl
+| LocalDecl.cdecl i id n t bi => LocalDecl.cdecl i id n (s.apply t) bi
+| LocalDecl.ldecl i id n t v  => LocalDecl.ldecl i id n (s.apply t) (s.apply v)
+
+abbrev Expr.applyFVarSubst (s : Meta.FVarSubst) (e : Expr) : Expr :=
+s.apply e
+
 end Lean

stage0/src/Lean/Meta/Tactic/Subst.lean

@@ -27,12 +27,14 @@ withMVarContext mvarId $ do
     a ← whnf a;
     match a with
     | Expr.fvar aFVarId _ => do
+      trace! `Meta.Tactic.subst ("substituting " ++ a ++ " (id: " ++ aFVarId ++ ") with " ++ b);
       mctx ← getMCtx;
       when (mctx.exprDependsOn b aFVarId) $
         throwTacticEx `subst mvarId ("'" ++ a ++ "' occurs at" ++ indentExpr b);
       aLocalDecl ← getLocalDecl aFVarId;
       (vars, mvarId) ← revert mvarId #[aFVarId, hFVarId] true;
       (twoVars, mvarId) ← introN mvarId 2 [] false;
+      trace! `Meta.Tactic.subst ("reverted variables " ++ toString vars);
       let aFVarId := twoVars.get! 0;
       let a       := mkFVar aFVarId;
       let hFVarId := twoVars.get! 1;
@@ -59,7 +61,7 @@ withMVarContext mvarId $ do
             (newFVars, mvarId) ← introN mvarId (vars.size - 2) [] false;
             fvarSubst ← newFVars.size.foldM
               (fun i (fvarSubst : FVarSubst) =>
-                let var      := vars.get! i;
+                let var      := vars.get! (i+2);
                 let newFVar := newFVars.get! i;
                 pure $ fvarSubst.insert var newFVar)
               FVarSubst.empty;

stage0/src/Lean/Meta/WHNF.lean

@@ -23,7 +23,7 @@ Lean.WHNF.whnfCore getConstNoEx isAuxDef? whnf inferType isExprDefEqAux getLocal
 unsafe def reduceNativeConst (α : Type) (typeName : Name) (constName : Name) : MetaM α := do
 env ← getEnv;
 match env.evalConstCheck α typeName constName with
-| Except.error ex => throw $ Exception.other ex
+| Except.error ex => throwOther ex
 | Except.ok v     => pure v
 
 unsafe def reduceBoolNativeUnsafe (constName : Name) : MetaM Bool := reduceNativeConst Bool `Bool constName
@@ -86,22 +86,30 @@ else match e with
 
 
 @[inline] private def useWHNFCache (e : Expr) : MetaM Bool := do
--- We cache only consed terms
+-- We cache only closed terms
 if e.hasFVar then pure false
 else do
   ctx ← read;
-  pure $ ctx.config.transparency == TransparencyMode.default
+  pure $ ctx.config.transparency != TransparencyMode.reducible
 
 @[inline] private def cached? (useCache : Bool) (e : Expr) : MetaM (Option Expr) := do
 if useCache then do
-  s ← get;
-  pure $ s.cache.whnfDefault.find? e
+  ctx ← read;
+  s   ← get;
+  match ctx.config.transparency with
+  | TransparencyMode.default => pure $ s.cache.whnfDefault.find? e
+  | TransparencyMode.all     => pure $ s.cache.whnfAll.find? e
+  | _                        => unreachable!
 else
   pure none
 
 private def cache (useCache : Bool) (e r : Expr) : MetaM Expr := do
+ctx ← read;
 when useCache $
-  modify $ fun s => { s with cache := { s.cache with whnfDefault := s.cache.whnfDefault.insert e r } };
+  match ctx.config.transparency with
+  | TransparencyMode.default => modify $ fun s => { s with cache := { s.cache with whnfDefault := s.cache.whnfDefault.insert e r } }
+  | TransparencyMode.all     => modify $ fun s => { s with cache := { s.cache with whnfAll := s.cache.whnfAll.insert e r } }
+  | _                        => unreachable!;
 pure r
 
 partial def whnfImpl : Expr → MetaM Expr

stage0/src/Lean/Parser/Term.lean

@@ -196,7 +196,7 @@ def namedArgument  := parser! try ("(" >> ident >> " := ") >> termParser >> ")"
 @[builtinTermParser] def orM         := tparser! infixR " <||> " 30
 @[builtinTermParser] def andM        := tparser! infixR " <&&> " 35
 @[builtinTermParser] def andthen     := tparser! infixR " >> "  60
-@[builtinTermParser] def bindOp      := tparser! infixR " >>= " 55
+@[builtinTermParser] def bindOp      := tparser! infixL " >>= " 55
 @[builtinTermParser] def mapRev      := tparser! infixR " <&> " 100
 @[builtinTermParser] def seq         := tparser! infixL " <*> " 60
 @[builtinTermParser] def seqLeft     := tparser! infixL " <* "  60

stage0/src/Lean/Util/Closure.lean

@@ -12,11 +12,11 @@ namespace Lean
 namespace Closure
 
 structure Context :=
-(mctx      : MetavarContext)
 (lctxInput : LocalContext)
 (zeta      : Bool) -- if `true` let-variables are expanded
 
 structure State :=
+(mctx          : MetavarContext)
 (lctxOutput    : LocalContext := {})
 (ngen          : NameGenerator := { namePrefix := `_closure })
 (visitedLevel  : LevelMap Level := {})
@@ -48,15 +48,19 @@ let p := (`u).appendIndexAfter s.nextLevelIdx;
 modify $ fun s => { s with levelParams := s.levelParams.push p, nextLevelIdx := s.nextLevelIdx + 1, levelClosure := s.levelClosure.push u };
 pure $ mkLevelParam p
 
+def getMCtx : ClosureM MetavarContext := do
+s ← get; pure s.mctx
+
+def instantiateMVars (e : Expr) : ClosureM Expr := do
+modifyGet fun s =>
+  let (e, mctx) := s.mctx.instantiateMVars e;
+  (e, { s with mctx := mctx })
+
 partial def collectLevelAux : Level → ClosureM Level
 | u@(Level.succ v _)      => do v ← visitLevel collectLevelAux v; pure $ u.updateSucc! v
 | u@(Level.max v w _)     => do v ← visitLevel collectLevelAux v; w ← visitLevel collectLevelAux w; pure $ u.updateMax! v w
 | u@(Level.imax v w _)    => do v ← visitLevel collectLevelAux v; w ← visitLevel collectLevelAux w; pure $ u.updateIMax! v w
-| u@(Level.mvar mvarId _) => do
-  ctx ← read;
-  match ctx.mctx.getLevelAssignment? mvarId with
-  | none   => mkNewLevelParam u
-  | some v => visitLevel collectLevelAux v
+| u@(Level.mvar mvarId _) => mkNewLevelParam u
 | u@(Level.param _ _)     => mkNewLevelParam u
 | u@(Level.zero _)        => pure u
 
@@ -119,37 +123,40 @@ partial def collectExprAux : Expr → ClosureM Expr
   | Expr.sort u _        => do u ← collectLevel u; pure (e.updateSort! u)
   | Expr.const c us _    => do us ← us.mapM collectLevel; pure (e.updateConst! us)
   | Expr.mvar mvarId _   => do
-    ctx ← read;
-    match ctx.mctx.findDecl? mvarId with
+    mctx ← getMCtx;
+    match mctx.findDecl? mvarId with
     | none          => throw "unknown metavariable"
-    | some mvarDecl =>
-      match ctx.mctx.getExprAssignment? mvarId with
-      | some v => collect v
-      | none   => do
-        type ← collect mvarDecl.type;
-        x    ← mkLocalDecl none type BinderInfo.default;
-        modify $ fun s => { s with exprClosure := s.exprClosure.push e };
-        pure x
+    | some mvarDecl => do
+      type ← instantiateMVars mvarDecl.type;
+      type ← collect type;
+      x    ← mkLocalDecl none type BinderInfo.default;
+      modify $ fun s => { s with exprClosure := s.exprClosure.push e };
+      pure x
   | Expr.fvar fvarId _ => do
     ctx ← read;
     match ctx.lctxInput.find? fvarId with
     | none => throw "unknown free variable"
     | some (LocalDecl.cdecl _ _ userName type bi) => do
+      type ← instantiateMVars type;
       type ← collect type;
       x    ← mkLocalDecl userName type bi;
       modify $ fun s => { s with exprClosure := s.exprClosure.push e };
       pure x
     | some (LocalDecl.ldecl _ _ userName type value) =>
-      if ctx.zeta then
+      if ctx.zeta then do
+        value ← instantiateMVars value;
         collect value
       else do
+        type  ← instantiateMVars type;
         type  ← collect type;
+        value ← instantiateMVars value;
         value ← collect value;
         -- Note that let-declarations do not need to be provided to the closure being constructed.
         mkLetDecl userName type value
   | e => pure e
 
-def collectExpr (e : Expr) : ClosureM Expr :=
+def collectExpr (e : Expr) : ClosureM Expr := do
+e ← instantiateMVars e;
 visitExpr collectExprAux e
 
 structure MkClosureResult :=
@@ -158,6 +165,7 @@ structure MkClosureResult :=
 (value        : Expr)
 (levelClosure : Array Level)
 (exprClosure  : Array Expr)
+(mctx         : MetavarContext)
 
 def mkClosure (mctx : MetavarContext) (lctx : LocalContext) (type : Expr) (value : Expr) (zeta : Bool := false) : Except String MkClosureResult :=
 let shareCommonTypeValue : Std.ShareCommonM (Expr × Expr) := do {
@@ -166,13 +174,14 @@ let shareCommonTypeValue : Std.ShareCommonM (Expr × Expr) := do {
   pure (type, value)
 };
 let (type, value) := shareCommonTypeValue.run;
-let mkTypeValue : ClosureM (Expr × Expr) := do {
+let mkTypeValue : ClosureM (Expr × Expr × MetavarContext) := do {
   type  ← collectExpr type;
   value ← collectExpr value;
-  pure (type, value)
+  mctx  ← getMCtx;
+  pure (type, value, mctx)
 };
-match (mkTypeValue { mctx := mctx, lctxInput := lctx, zeta := zeta }).run {} with
-| EStateM.Result.ok (type, value) s =>
+match (mkTypeValue { lctxInput := lctx, zeta := zeta }).run { mctx := mctx } with
+| EStateM.Result.ok (type, value, mctx) s =>
   let fvars := s.lctxOutput.getFVars;
   let type  := s.lctxOutput.mkForall fvars type;
   let value := s.lctxOutput.mkLambda fvars value;
@@ -181,13 +190,14 @@ match (mkTypeValue { mctx := mctx, lctxInput := lctx, zeta := zeta }).run {} wit
     type         := type,
     value        := value,
     levelClosure := s.levelClosure,
-    exprClosure  := s.exprClosure }
+    exprClosure  := s.exprClosure,
+    mctx         := mctx }
 | EStateM.Result.error ex s => Except.error ex
 
 end Closure
 
 def mkAuxDefinition (env : Environment) (opts : Options) (mctx : MetavarContext) (lctx : LocalContext) (name : Name) (type : Expr) (value : Expr)
-    (zeta : Bool := false) : Except KernelException (Expr × Environment) :=
+    (zeta : Bool := false) : Except KernelException (Expr × Environment × MetavarContext) :=
 match Closure.mkClosure mctx lctx type value zeta with
 | Except.error ex  => throw $ KernelException.other ex
 | Except.ok result => do
@@ -201,6 +211,6 @@ match Closure.mkClosure mctx lctx type value zeta with
   };
   env ← env.addAndCompile opts decl;
   let c := mkAppN (mkConst name result.levelClosure.toList) result.exprClosure;
-  pure (c, env)
+  pure (c, env, result.mctx)
 
 end Lean

stage0/stdlib/Lean/Expr.c

@@ -6885,10 +6885,12 @@ return x_4;
 lean_object* l_Lean_Expr_replaceFVarId(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
-lean_object* x_4; lean_object* x_5; 
+lean_object* x_4; lean_object* x_5; lean_object* x_6; 
 x_4 = l_Lean_mkFVar(x_2);
-x_5 = l_Lean_Expr_replaceFVar(x_1, x_4, x_3);
-return x_5;
+x_5 = l_Lean_mkFVar(x_3);
+x_6 = l_Lean_Expr_replaceFVar(x_1, x_4, x_5);
+lean_dec(x_5);
+return x_6;
 }
 }
 lean_object* l_Lean_Expr_replaceFVarId___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
@@ -6896,7 +6898,6 @@ _start:
 {
 lean_object* x_4; 
 x_4 = l_Lean_Expr_replaceFVarId(x_1, x_2, x_3);
-lean_dec(x_3);
 lean_dec(x_1);
 return x_4;
 }

stage0/stdlib/Lean/Meta/Tactic/Cases.c

@@ -25,6 +25,7 @@ lean_object* l_Lean_Expr_withAppAux___main___at_Lean_Meta_generalizeIndices___sp
 extern lean_object* l_Lean_Expr_eq_x3f___closed__2;
 lean_object* l_Lean_Expr_mvarId_x21(lean_object*);
 lean_object* l___private_Lean_Meta_Tactic_Cases_5__hasIndepIndices(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_registerTraceClass(lean_object*, lean_object*);
 lean_object* l___private_Lean_Meta_Tactic_Cases_8__unifyEqsAux___main___closed__1;
 lean_object* lean_mk_empty_array_with_capacity(lean_object*);
 lean_object* l___private_Lean_Meta_Tactic_Cases_2__withNewIndexEqsAux___main(lean_object*);
@@ -81,7 +82,6 @@ lean_object* l_Nat_anyAux___main___at___private_Lean_Meta_Tactic_Cases_5__hasInd
 lean_object* l_Array_umapMAux___main___at___private_Lean_Meta_Tactic_Cases_8__unifyEqsAux___main___spec__2(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_MetavarContext_8__dep___main___at___private_Lean_Meta_Tactic_Cases_5__hasIndepIndices___spec__36(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Expr_appFn_x21(lean_object*);
-extern lean_object* l___private_Lean_Meta_Basic_11__regTraceClasses___closed__2;
 lean_object* l_Std_PersistentArray_anyMAux___main___at___private_Lean_Meta_Tactic_Cases_5__hasIndepIndices___spec__14___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_push(lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
@@ -277,6 +277,7 @@ lean_object* l_Array_umapMAux___main___at___private_Lean_Meta_Tactic_Cases_8__un
 uint8_t l_Array_anyRangeMAux___main___at___private_Lean_Meta_Tactic_Cases_5__hasIndepIndices___spec__10(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Meta_Tactic_Cases_9__unifyEqs___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Array_anyRangeMAux___main___at___private_Lean_Meta_Tactic_Cases_5__hasIndepIndices___spec__44(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+extern lean_object* l___private_Lean_Meta_Tactic_Util_1__regTraceClasses___closed__2;
 lean_object* l_Array_umapMAux___main___at___private_Lean_Meta_Tactic_Cases_8__unifyEqsAux___main___spec__9___boxed(lean_object*, lean_object*, lean_object*);
 uint8_t l_Array_anyRangeMAux___main___at___private_Lean_Meta_Tactic_Cases_5__hasIndepIndices___spec__45(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Expr_withAppAux___main___at___private_Lean_Meta_Tactic_Cases_4__mkCasesContext_x3f___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -310,6 +311,7 @@ uint8_t l_Std_PersistentArray_anyMAux___main___at___private_Lean_Meta_Tactic_Cas
 lean_object* l_Array_umapMAux___main___at___private_Lean_Meta_Tactic_Cases_8__unifyEqsAux___main___spec__3___boxed(lean_object*, lean_object*, lean_object*);
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_cases___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l___private_Lean_Meta_Tactic_Cases_10__regTraceClasses(lean_object*);
 lean_object* l___private_Lean_Meta_Tactic_Cases_1__mkEqAndProof(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
@@ -12675,7 +12677,7 @@ lean_object* _init_l___private_Lean_Meta_Tactic_Cases_8__unifyEqsAux___main___cl
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l___private_Lean_Meta_Basic_11__regTraceClasses___closed__2;
+x_1 = l___private_Lean_Meta_Tactic_Util_1__regTraceClasses___closed__2;
 x_2 = l___private_Lean_Meta_Tactic_Cases_8__unifyEqsAux___main___lambda__1___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
@@ -13930,6 +13932,15 @@ lean_dec(x_5);
 return x_8;
 }
 }
+lean_object* l___private_Lean_Meta_Tactic_Cases_10__regTraceClasses(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; 
+x_2 = l___private_Lean_Meta_Tactic_Cases_8__unifyEqsAux___main___closed__1;
+x_3 = l_Lean_registerTraceClass(x_2, x_1);
+return x_3;
+}
+}
 lean_object* initialize_Init(lean_object*);
 lean_object* initialize_Lean_Meta_AppBuilder(lean_object*);
 lean_object* initialize_Lean_Meta_Tactic_Induction(lean_object*);
@@ -14019,6 +14030,9 @@ l_Lean_Meta_Cases_cases___lambda__1___closed__6 = _init_l_Lean_Meta_Cases_cases_
 lean_mark_persistent(l_Lean_Meta_Cases_cases___lambda__1___closed__6);
 l_Lean_Meta_Cases_cases___lambda__1___closed__7 = _init_l_Lean_Meta_Cases_cases___lambda__1___closed__7();
 lean_mark_persistent(l_Lean_Meta_Cases_cases___lambda__1___closed__7);
+res = l___private_Lean_Meta_Tactic_Cases_10__regTraceClasses(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 return lean_mk_io_result(lean_box(0));
 }
 #ifdef __cplusplus

stage0/stdlib/Lean/Meta/Tactic/FVarSubst.c

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Lean.Meta.Tactic.FVarSubst
-// Imports: Init Lean.Expr Lean.Util.ReplaceExpr
+// Imports: Init Lean.Expr Lean.LocalContext Lean.Util.ReplaceExpr
 #include <lean/lean.h>
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -15,6 +15,7 @@ extern "C" {
 #endif
 lean_object* lean_expr_update_forall(lean_object*, uint8_t, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_FVarSubst_apply___boxed(lean_object*, lean_object*);
+lean_object* l_Std_RBNode_fold___main___at_Lean_Meta_FVarSubst_domain___spec__1___boxed(lean_object*, lean_object*);
 lean_object* l_unreachable_x21___rarg(lean_object*);
 uint8_t l_USize_decEq(size_t, size_t);
 lean_object* lean_array_uget(lean_object*, size_t);
@@ -22,12 +23,16 @@ lean_object* lean_expr_update_mdata(lean_object*, lean_object*);
 uint8_t l_Lean_Name_quickLt(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_FVarSubst_erase(lean_object*, lean_object*);
 lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
+lean_object* l_Lean_Meta_FVarSubst_domain(lean_object*);
 lean_object* l_Std_RBNode_find___main___at_Lean_Meta_FVarSubst_get___spec__1___boxed(lean_object*, lean_object*);
+lean_object* l_Lean_Expr_applyFVarSubst___boxed(lean_object*, lean_object*);
+lean_object* l_Lean_Meta_FVarSubst_domain___boxed(lean_object*);
 uint8_t l_Lean_NameMap_contains___rarg(lean_object*, lean_object*);
 lean_object* l_Std_RBNode_erase___at_Lean_Meta_FVarSubst_erase___spec__1(lean_object*, lean_object*);
 lean_object* l_Std_RBNode_del___main___at_Lean_Meta_FVarSubst_erase___spec__2(lean_object*, lean_object*);
 lean_object* l_Std_RBNode_fold___main___at_Lean_Meta_FVarSubst_compose___spec__1(lean_object*, lean_object*);
 lean_object* l_Std_RBNode_setBlack___rarg(lean_object*);
+lean_object* l_Std_RBNode_fold___main___at_Lean_Meta_FVarSubst_domain___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_FVarSubst_apply(lean_object*, lean_object*);
 lean_object* l_Std_RBNode_balRight___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Std_RBNode_isBlack___rarg(lean_object*);
@@ -41,6 +46,7 @@ lean_object* l_Std_RBNode_appendTrees___main___rarg(lean_object*, lean_object*);
 lean_object* lean_expr_update_let(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkFVar(lean_object*);
 uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
+lean_object* l_Lean_LocalDecl_applyFVarSubst___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_FVarSubst_contains___boxed(lean_object*, lean_object*);
 lean_object* lean_expr_update_proj(lean_object*, lean_object*);
 lean_object* l_Std_RBNode_erase___at_Lean_Meta_FVarSubst_erase___spec__1___boxed(lean_object*, lean_object*);
@@ -56,8 +62,10 @@ lean_object* l_Lean_Meta_FVarSubst_erase___boxed(lean_object*, lean_object*);
 lean_object* l_Std_RBNode_del___main___at_Lean_Meta_FVarSubst_erase___spec__2___boxed(lean_object*, lean_object*);
 lean_object* lean_expr_update_app(lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Expr_hasFVar(lean_object*);
+lean_object* l_Lean_LocalDecl_applyFVarSubst(lean_object*, lean_object*);
 lean_object* l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___at_Lean_Meta_FVarSubst_apply___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Expr_ReplaceImpl_initCache;
+lean_object* l_Lean_Expr_applyFVarSubst(lean_object*, lean_object*);
 lean_object* _init_l_Lean_Meta_FVarSubst_empty() {
 _start:
 {
@@ -992,8 +1000,166 @@ return x_3;
 }
 }
 }
+lean_object* l_Std_RBNode_fold___main___at_Lean_Meta_FVarSubst_domain___spec__1(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+if (lean_obj_tag(x_2) == 0)
+{
+return x_1;
+}
+else
+{
+lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; 
+x_3 = lean_ctor_get(x_2, 0);
+x_4 = lean_ctor_get(x_2, 1);
+x_5 = lean_ctor_get(x_2, 3);
+x_6 = l_Std_RBNode_fold___main___at_Lean_Meta_FVarSubst_domain___spec__1(x_1, x_3);
+lean_inc(x_4);
+x_7 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_7, 0, x_4);
+lean_ctor_set(x_7, 1, x_6);
+x_1 = x_7;
+x_2 = x_5;
+goto _start;
+}
+}
+}
+lean_object* l_Lean_Meta_FVarSubst_domain(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; lean_object* x_3; 
+x_2 = lean_box(0);
+x_3 = l_Std_RBNode_fold___main___at_Lean_Meta_FVarSubst_domain___spec__1(x_2, x_1);
+return x_3;
+}
+}
+lean_object* l_Std_RBNode_fold___main___at_Lean_Meta_FVarSubst_domain___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_Std_RBNode_fold___main___at_Lean_Meta_FVarSubst_domain___spec__1(x_1, x_2);
+lean_dec(x_2);
+return x_3;
+}
+}
+lean_object* l_Lean_Meta_FVarSubst_domain___boxed(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = l_Lean_Meta_FVarSubst_domain(x_1);
+lean_dec(x_1);
+return x_2;
+}
+}
+lean_object* l_Lean_LocalDecl_applyFVarSubst(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+if (lean_obj_tag(x_2) == 0)
+{
+uint8_t x_3; 
+x_3 = !lean_is_exclusive(x_2);
+if (x_3 == 0)
+{
+lean_object* x_4; lean_object* x_5; 
+x_4 = lean_ctor_get(x_2, 3);
+x_5 = l_Lean_Meta_FVarSubst_apply(x_1, x_4);
+lean_ctor_set(x_2, 3, x_5);
+return x_2;
+}
+else
+{
+lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10; lean_object* x_11; lean_object* x_12; 
+x_6 = lean_ctor_get(x_2, 0);
+x_7 = lean_ctor_get(x_2, 1);
+x_8 = lean_ctor_get(x_2, 2);
+x_9 = lean_ctor_get(x_2, 3);
+x_10 = lean_ctor_get_uint8(x_2, sizeof(void*)*4);
+lean_inc(x_9);
+lean_inc(x_8);
+lean_inc(x_7);
+lean_inc(x_6);
+lean_dec(x_2);
+x_11 = l_Lean_Meta_FVarSubst_apply(x_1, x_9);
+x_12 = lean_alloc_ctor(0, 4, 1);
+lean_ctor_set(x_12, 0, x_6);
+lean_ctor_set(x_12, 1, x_7);
+lean_ctor_set(x_12, 2, x_8);
+lean_ctor_set(x_12, 3, x_11);
+lean_ctor_set_uint8(x_12, sizeof(void*)*4, x_10);
+return x_12;
+}
+}
+else
+{
+uint8_t x_13; 
+x_13 = !lean_is_exclusive(x_2);
+if (x_13 == 0)
+{
+lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; 
+x_14 = lean_ctor_get(x_2, 3);
+x_15 = lean_ctor_get(x_2, 4);
+x_16 = l_Lean_Meta_FVarSubst_apply(x_1, x_14);
+x_17 = l_Lean_Meta_FVarSubst_apply(x_1, x_15);
+lean_ctor_set(x_2, 4, x_17);
+lean_ctor_set(x_2, 3, x_16);
+return x_2;
+}
+else
+{
+lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; 
+x_18 = lean_ctor_get(x_2, 0);
+x_19 = lean_ctor_get(x_2, 1);
+x_20 = lean_ctor_get(x_2, 2);
+x_21 = lean_ctor_get(x_2, 3);
+x_22 = lean_ctor_get(x_2, 4);
+lean_inc(x_22);
+lean_inc(x_21);
+lean_inc(x_20);
+lean_inc(x_19);
+lean_inc(x_18);
+lean_dec(x_2);
+x_23 = l_Lean_Meta_FVarSubst_apply(x_1, x_21);
+x_24 = l_Lean_Meta_FVarSubst_apply(x_1, x_22);
+x_25 = lean_alloc_ctor(1, 5, 0);
+lean_ctor_set(x_25, 0, x_18);
+lean_ctor_set(x_25, 1, x_19);
+lean_ctor_set(x_25, 2, x_20);
+lean_ctor_set(x_25, 3, x_23);
+lean_ctor_set(x_25, 4, x_24);
+return x_25;
+}
+}
+}
+}
+lean_object* l_Lean_LocalDecl_applyFVarSubst___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_Lean_LocalDecl_applyFVarSubst(x_1, x_2);
+lean_dec(x_1);
+return x_3;
+}
+}
+lean_object* l_Lean_Expr_applyFVarSubst(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_Lean_Meta_FVarSubst_apply(x_1, x_2);
+return x_3;
+}
+}
+lean_object* l_Lean_Expr_applyFVarSubst___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_Lean_Expr_applyFVarSubst(x_1, x_2);
+lean_dec(x_1);
+return x_3;
+}
+}
 lean_object* initialize_Init(lean_object*);
 lean_object* initialize_Lean_Expr(lean_object*);
+lean_object* initialize_Lean_LocalContext(lean_object*);
 lean_object* initialize_Lean_Util_ReplaceExpr(lean_object*);
 static bool _G_initialized = false;
 lean_object* initialize_Lean_Meta_Tactic_FVarSubst(lean_object* w) {
@@ -1006,6 +1172,9 @@ lean_dec_ref(res);
 res = initialize_Lean_Expr(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Lean_LocalContext(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 res = initialize_Lean_Util_ReplaceExpr(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);

stage0/stdlib/Lean/Parser/Term.c

@@ -52610,7 +52610,7 @@ _start:
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Term_bindOp___elambda__1___closed__3;
 x_2 = lean_unsigned_to_nat(55u);
-x_3 = l_Lean_Parser_Term_infixR(x_1, x_2);
+x_3 = l_Lean_Parser_Term_infixL(x_1, x_2);
 return x_3;
 }
 }