chore: update stage0

stage0/src/Lean/Elab/Binders.lean

@@ -388,8 +388,7 @@ def elabLetDeclAux (n : Name) (binders : Array Syntax) (typeStx : Syntax) (valSt
     (expectedType? : Option Expr) (useLetExpr : Bool) : TermElabM Expr := do
 (type, val) ← elabBinders binders $ fun xs => do {
   type ← elabType typeStx;
-  val  ← elabTerm valStx type;
-  val  ← withRef valStx $ ensureHasType type val;
+  val  ← elabTermEnsuringType valStx type;
   type ← mkForall xs type;
   val  ← mkLambda xs val;
   pure (type, val)

stage0/src/Lean/Elab/DoNotation.lean

@@ -194,16 +194,14 @@ private partial def processDoElemsAux (doElems : Array Syntax) (m bindInstVal :
     let actionStx := doElem.getArg 3;
     type ← elabType typeStx;
     let actionExpectedType := mkApp m type;
-    action ← elabTerm actionStx actionExpectedType;
-    action ← withRef actionStx $ ensureHasType actionExpectedType action;
+    action ← elabTermEnsuringType actionStx actionExpectedType;
     withLocalDecl id BinderInfo.default type $ fun x =>
       processDoElemsAux (i+1) (elems.push { action := action, var := x })
   else if doElem.getKind == `Lean.Parser.Term.doExpr then do
     when (i != doElems.size - 1) $
       throwError ("unexpected 'do' expression element" ++ Format.line ++ doElem);
     let bodyStx := doElem.getArg 0;
-    body ← elabTerm bodyStx expectedType;
-    body ← ensureHasType expectedType body;
+    body ← elabTermEnsuringType bodyStx expectedType;
     mkBind m bindInstVal elems body
   else
     throwError ("unexpected 'do' expression element" ++ Format.line ++ doElem)

stage0/src/Lean/Elab/Match.lean

@@ -66,8 +66,7 @@ private partial def elabDiscrsAux (discrStxs : Array Syntax) (expectedType : Exp
     matchType ← whnf matchType;
     match matchType with
     | Expr.forallE _ d b _ => do
-      discr ← elabTerm discrStx d;
-      discr ← ensureHasType d discr;
+      discr ← elabTermEnsuringType discrStx d;
       trace `Elab.match fun _ => "discr #" ++ toString i ++ " " ++ discr ++ " : " ++ d;
       elabDiscrsAux (i+1) (b.instantiate1 discr) (discrs.push discr)
     | _ => throwError ("invalid type provided to match-expression, function type with arity #" ++ toString discrStxs ++ " expected")
@@ -377,8 +376,7 @@ private partial def elabPatternsAux (patternStxs : Array Syntax) : Nat → Expr
     match matchType with
     | Expr.forallE _ d b _ => do
       let patternStx := patternStxs.get ⟨i, h⟩;
-      pattern ← elabTerm patternStx d;
-      pattern ← withRef patternStx $ ensureHasType d pattern;
+      pattern ← elabTermEnsuringType patternStx d;
       elabPatternsAux (i+1) (b.instantiate1 pattern) (patterns.push pattern)
     | _ => throwError "unexpected match type"
   else
@@ -516,7 +514,7 @@ withRef alt.ref do
 trace `Elab.match fun _ => "patternVars: " ++ toString patternVars;
 withPatternVars patternVars fun patternVarDecls => do
   (altLHS, matchType) ← elabPatterns patternVarDecls alt.patterns matchType;
-  rhs ← elabTerm alt.rhs matchType;
+  rhs ← elabTermEnsuringType alt.rhs matchType;
   let xs := altLHS.fvarDecls.toArray.map LocalDecl.toExpr;
   rhs ← if xs.isEmpty then pure $ mkThunk rhs else mkLambda xs rhs;
   trace `Elab.match fun _ => "rhs: " ++ rhs;

stage0/src/Lean/Elab/StructInst.lean

@@ -512,7 +512,7 @@ private partial def elabStruct : Struct → Option Expr → TermElabM (Expr × S
             pure (e, type, field::fields)
           };
           match field.val with
-          | FieldVal.term stx => do val ← elabTerm stx (some d); val ← withRef stx $ ensureHasType d val; continue val field
+          | FieldVal.term stx => do val ← elabTermEnsuringType stx d; continue val field
           | FieldVal.nested s => do (val, sNew) ← elabStruct s (some d); val ← ensureHasType d val; continue val { field with val := FieldVal.nested sNew }
           | FieldVal.default  => do val ← withRef field.ref $ mkFreshExprMVar (some d); continue (markDefaultMissing val) field
         | _ => withRef field.ref $ throwFailedToElabField fieldName s.structName ("unexpected constructor type" ++ indentExpr type)

stage0/src/Lean/Elab/Structure.lean

@@ -289,8 +289,7 @@ private partial def withFields {α} (views : Array StructFieldView) : Nat → Ar
           when (!view.binders.getArgs.isEmpty || view.type?.isSome) $
             Term.throwErrorAt view.type?.get! ("omit field '" ++ view.name ++ "' type to set default value");
           fvarType ← Term.inferType info.fvar;
-          value ← Term.elabTerm valStx fvarType;
-          value ← Term.withRef valStx $ Term.ensureHasType fvarType value;
+          value ← Term.elabTermEnsuringType valStx fvarType;
           let infos := infos.push { info with value? := value };
           withFields (i+1) infos k
       | StructFieldKind.subobject => unreachable!

stage0/src/Lean/Elab/SyntheticMVars.lean

@@ -52,7 +52,7 @@ withRef stx $ withMVarContext mvarId $ do
       result       ← resumeElabTerm stx expectedType (!postponeOnError);
       /- We must ensure `result` has the expected type because it is the one expected by the method that postponed stx.
          That is, the method does not have an opportunity to check whether `result` has the expected type or not. -/
-      result ← ensureHasType expectedType result;
+      result ← withRef stx $ ensureHasType expectedType result;
       assignExprMVar mvarId result;
       pure true)
     (fun ex => match ex with

stage0/src/Lean/Elab/Term.lean

@@ -752,7 +752,9 @@ when ctx.mayPostpone $ throw Exception.postpone
 
 /-- If `mayPostpone == true` and `e`'s head is a metavariable, throw `Exception.postpone`. -/
 def tryPostponeIfMVar (e : Expr) : TermElabM Unit := do
-when e.getAppFn.isMVar $ tryPostpone
+when e.getAppFn.isMVar do
+  e ← instantiateMVars e;
+  when e.getAppFn.isMVar $ tryPostpone
 
 def tryPostponeIfNoneOrMVar (e? : Option Expr) : TermElabM Unit :=
 match e? with
@@ -909,6 +911,10 @@ partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone : Bool) (
 def elabTerm (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) : TermElabM Expr :=
 withRef stx $ elabTermAux expectedType? catchExPostpone true stx
 
+def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
+e ← elabTerm stx expectedType?;
+withRef stx $ ensureHasType expectedType? e
+
 def elabTermWithoutImplicitLambdas (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) : TermElabM Expr := do
 elabTermAux expectedType? catchExPostpone false stx
 

stage0/src/Lean/Meta/ExprDefEq.lean

@@ -911,6 +911,21 @@ private def isLetFVar (fvarId : FVarId) : MetaM Bool := do
 decl ← getLocalDecl fvarId;
 pure decl.isLet
 
+private def isDefEqProofIrrel (t s : Expr) : MetaM LBool := do
+status ← isProofQuick t;
+match status with
+| LBool.false =>
+  pure LBool.undef
+| LBool.true  => do
+  tType ← inferType t;
+  sType ← inferType s;
+  toLBoolM $ isExprDefEqAux tType sType
+| LBool.undef => do
+  tType ← inferType t;
+  condM (isProp tType)
+    (do sType ← inferType s; toLBoolM $ isExprDefEqAux tType sType)
+    (pure LBool.undef)
+
 private partial def isDefEqQuick : Expr → Expr → MetaM LBool
 | Expr.lit  l₁ _,           Expr.lit l₂ _            => pure (l₁ == l₂).toLBool
 | Expr.sort u _,            Expr.sort v _            => toLBoolM $ isLevelDefEqAux u v
@@ -918,10 +933,10 @@ private partial def isDefEqQuick : Expr → Expr → MetaM LBool
 | t@(Expr.forallE _ _ _ _), s@(Expr.forallE _ _ _ _) => if t == s then pure LBool.true else toLBoolM $ isDefEqBinding t s
 | Expr.mdata _ t _,         s                        => isDefEqQuick t s
 | t,                        Expr.mdata _ s _         => isDefEqQuick t s
-| Expr.fvar fvarId₁ _,      Expr.fvar fvarId₂ _      =>
+| t@(Expr.fvar fvarId₁ _),  s@(Expr.fvar fvarId₂ _)  =>
   condM (isLetFVar fvarId₁ <||> isLetFVar fvarId₂)
     (pure LBool.undef)
-    (pure (fvarId₁ == fvarId₂).toLBool)
+    (if fvarId₁ == fvarId₂ then pure LBool.true else isDefEqProofIrrel t s)
 | t, s =>
   cond (t == s) (pure LBool.true) $
   cond (etaEq t s || etaEq s t) (pure LBool.true) $  -- t =?= (fun xs => t xs)
@@ -961,21 +976,6 @@ private partial def isDefEqQuick : Expr → Expr → MetaM LBool
     condM (commitWhen (processAssignment t s)) (pure LBool.true) $
     assign s t
 
-private def isDefEqProofIrrel (t s : Expr) : MetaM LBool := do
-status ← isProofQuick t;
-match status with
-| LBool.false =>
-  pure LBool.undef
-| LBool.true  => do
-  tType ← inferType t;
-  sType ← inferType s;
-  toLBoolM $ isExprDefEqAux tType sType
-| LBool.undef => do
-  tType ← inferType t;
-  condM (isProp tType)
-    (do sType ← inferType s; toLBoolM $ isExprDefEqAux tType sType)
-    (pure LBool.undef)
-
 @[inline] def whenUndefDo (x : MetaM LBool) (k : MetaM Bool) : MetaM Bool := do
 status ← x;
 match status with

stage0/src/frontends/lean/builtin_exprs.cpp

@@ -347,7 +347,9 @@ static expr parse_do(parser & p, bool has_braces) {
                                    pos);
             }
         } else {
-            r = p.rec_save_pos(mk_app(p.save_pos(mk_const({"HasSeqRight", "seqRight"}), ps[i]), es[i], r), ps[i]);
+            expr action2 = p.save_pos(mk_lambda("_", mk_expr_placeholder(), r), ps[i]);
+            r = p.rec_save_pos(mk_app(p.save_pos(mk_bind_fn(p), ps[i]), es[i], action2), ps[i]);
+            // r = p.rec_save_pos(mk_app(p.save_pos(mk_const({"HasSeqRight", "seqRight"}), ps[i]), es[i], r), ps[i]);
         }
     }
     return r;

stage0/stdlib/Lean/Elab/App.c

@@ -13455,6 +13455,8 @@ block_37:
 if (x_17 == 0)
 {
 lean_object* x_19; 
+lean_inc(x_6);
+lean_inc(x_12);
 x_19 = l_Lean_Elab_Term_tryPostponeIfMVar(x_12, x_6, x_18);
 if (lean_obj_tag(x_19) == 0)
 {
@@ -15757,6 +15759,8 @@ lean_inc(x_8);
 x_9 = lean_ctor_get(x_7, 1);
 lean_inc(x_9);
 lean_dec(x_7);
+lean_inc(x_5);
+lean_inc(x_8);
 x_10 = l_Lean_Elab_Term_tryPostponeIfMVar(x_8, x_5, x_9);
 if (lean_obj_tag(x_10) == 0)
 {

stage0/stdlib/Lean/Elab/Binders.c

@@ -91,7 +91,6 @@ extern lean_object* l_Lean_mkAppStx___closed__7;
 lean_object* lean_nat_add(lean_object*, lean_object*);
 lean_object* l___private_Lean_Elab_Binders_9__getFunBinderIdsAux_x3f___main(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_matchDiscr___elambda__1___closed__2;
-lean_object* l_Lean_Elab_Term_ensureHasType(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Term_quoteAutoTactic___main___spec__1___closed__2;
 lean_object* l___private_Lean_Elab_Binders_3__expandOptIdent___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_mkFreshAnonymousIdent(lean_object*, lean_object*, lean_object*);
@@ -106,6 +105,7 @@ lean_object* l_Lean_Syntax_isSimpleTermId_x3f(lean_object*, uint8_t);
 lean_object* l_Lean_Elab_Term_FunBinders_elabFunBindersAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_quoteAutoTactic___main___closed__3;
 lean_object* l___private_Lean_Elab_Binders_11__expandFunBindersAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_elabTermEnsuringType(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_fget(lean_object*, lean_object*);
 extern lean_object* l_Lean_Expr_getOptParamDefault_x3f___closed__2;
 lean_object* l___private_Lean_Elab_Binders_4__expandBinderModifier___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -22701,7 +22701,7 @@ lean_inc(x_4);
 x_6 = l_Lean_Elab_Term_elabType(x_1, x_4, x_5);
 if (lean_obj_tag(x_6) == 0)
 {
-lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10; lean_object* x_11; 
+lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; 
 x_7 = lean_ctor_get(x_6, 0);
 lean_inc(x_7);
 x_8 = lean_ctor_get(x_6, 1);
@@ -22710,238 +22710,158 @@ lean_dec(x_6);
 lean_inc(x_7);
 x_9 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_9, 0, x_7);
-x_10 = 1;
 lean_inc(x_4);
-lean_inc(x_9);
-lean_inc(x_2);
-x_11 = l_Lean_Elab_Term_elabTerm(x_2, x_9, x_10, x_4, x_8);
-if (lean_obj_tag(x_11) == 0)
+x_10 = l_Lean_Elab_Term_elabTermEnsuringType(x_2, x_9, x_4, x_8);
+if (lean_obj_tag(x_10) == 0)
 {
-lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; uint8_t x_23; uint8_t x_24; uint8_t x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; 
-x_12 = lean_ctor_get(x_11, 0);
+lean_object* x_11; lean_object* x_12; lean_object* x_13; 
+x_11 = lean_ctor_get(x_10, 0);
+lean_inc(x_11);
+x_12 = lean_ctor_get(x_10, 1);
 lean_inc(x_12);
-x_13 = lean_ctor_get(x_11, 1);
-lean_inc(x_13);
-lean_dec(x_11);
-x_14 = lean_ctor_get(x_4, 0);
-lean_inc(x_14);
-x_15 = lean_ctor_get(x_4, 1);
-lean_inc(x_15);
-x_16 = lean_ctor_get(x_4, 2);
-lean_inc(x_16);
-x_17 = lean_ctor_get(x_4, 3);
-lean_inc(x_17);
-x_18 = lean_ctor_get(x_4, 4);
-lean_inc(x_18);
-x_19 = lean_ctor_get(x_4, 5);
-lean_inc(x_19);
-x_20 = lean_ctor_get(x_4, 6);
-lean_inc(x_20);
-x_21 = lean_ctor_get(x_4, 7);
-lean_inc(x_21);
-x_22 = lean_ctor_get(x_4, 8);
-lean_inc(x_22);
-x_23 = lean_ctor_get_uint8(x_4, sizeof(void*)*10);
-x_24 = lean_ctor_get_uint8(x_4, sizeof(void*)*10 + 1);
-x_25 = lean_ctor_get_uint8(x_4, sizeof(void*)*10 + 2);
-x_26 = lean_ctor_get(x_4, 9);
-lean_inc(x_26);
-x_27 = l_Lean_Elab_replaceRef(x_2, x_26);
-lean_dec(x_26);
-lean_dec(x_2);
-x_28 = lean_alloc_ctor(0, 10, 3);
-lean_ctor_set(x_28, 0, x_14);
-lean_ctor_set(x_28, 1, x_15);
-lean_ctor_set(x_28, 2, x_16);
-lean_ctor_set(x_28, 3, x_17);
-lean_ctor_set(x_28, 4, x_18);
-lean_ctor_set(x_28, 5, x_19);
-lean_ctor_set(x_28, 6, x_20);
-lean_ctor_set(x_28, 7, x_21);
-lean_ctor_set(x_28, 8, x_22);
-lean_ctor_set(x_28, 9, x_27);
-lean_ctor_set_uint8(x_28, sizeof(void*)*10, x_23);
-lean_ctor_set_uint8(x_28, sizeof(void*)*10 + 1, x_24);
-lean_ctor_set_uint8(x_28, sizeof(void*)*10 + 2, x_25);
-x_29 = l_Lean_Elab_Term_ensureHasType(x_9, x_12, x_28, x_13);
-if (lean_obj_tag(x_29) == 0)
-{
-lean_object* x_30; lean_object* x_31; lean_object* x_32; 
-x_30 = lean_ctor_get(x_29, 0);
-lean_inc(x_30);
-x_31 = lean_ctor_get(x_29, 1);
-lean_inc(x_31);
-lean_dec(x_29);
+lean_dec(x_10);
 lean_inc(x_4);
 lean_inc(x_3);
-x_32 = l_Lean_Elab_Term_mkForall(x_3, x_7, x_4, x_31);
-if (lean_obj_tag(x_32) == 0)
+x_13 = l_Lean_Elab_Term_mkForall(x_3, x_7, x_4, x_12);
+if (lean_obj_tag(x_13) == 0)
+{
+lean_object* x_14; lean_object* x_15; lean_object* x_16; 
+x_14 = lean_ctor_get(x_13, 0);
+lean_inc(x_14);
+x_15 = lean_ctor_get(x_13, 1);
+lean_inc(x_15);
+lean_dec(x_13);
+x_16 = l_Lean_Elab_Term_mkLambda(x_3, x_11, x_4, x_15);
+if (lean_obj_tag(x_16) == 0)
+{
+uint8_t x_17; 
+x_17 = !lean_is_exclusive(x_16);
+if (x_17 == 0)
+{
+lean_object* x_18; lean_object* x_19; 
+x_18 = lean_ctor_get(x_16, 0);
+x_19 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_19, 0, x_14);
+lean_ctor_set(x_19, 1, x_18);
+lean_ctor_set(x_16, 0, x_19);
+return x_16;
+}
+else
+{
+lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; 
+x_20 = lean_ctor_get(x_16, 0);
+x_21 = lean_ctor_get(x_16, 1);
+lean_inc(x_21);
+lean_inc(x_20);
+lean_dec(x_16);
+x_22 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_22, 0, x_14);
+lean_ctor_set(x_22, 1, x_20);
+x_23 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_23, 0, x_22);
+lean_ctor_set(x_23, 1, x_21);
+return x_23;
+}
+}
+else
+{
+uint8_t x_24; 
+lean_dec(x_14);
+x_24 = !lean_is_exclusive(x_16);
+if (x_24 == 0)
+{
+return x_16;
+}
+else
+{
+lean_object* x_25; lean_object* x_26; lean_object* x_27; 
+x_25 = lean_ctor_get(x_16, 0);
+x_26 = lean_ctor_get(x_16, 1);
+lean_inc(x_26);
+lean_inc(x_25);
+lean_dec(x_16);
+x_27 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_27, 0, x_25);
+lean_ctor_set(x_27, 1, x_26);
+return x_27;
+}
+}
+}
+else
+{
+uint8_t x_28; 
+lean_dec(x_11);
+lean_dec(x_4);
+lean_dec(x_3);
+x_28 = !lean_is_exclusive(x_13);
+if (x_28 == 0)
+{
+return x_13;
+}
+else
+{
+lean_object* x_29; lean_object* x_30; lean_object* x_31; 
+x_29 = lean_ctor_get(x_13, 0);
+x_30 = lean_ctor_get(x_13, 1);
+lean_inc(x_30);
+lean_inc(x_29);
+lean_dec(x_13);
+x_31 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_31, 0, x_29);
+lean_ctor_set(x_31, 1, x_30);
+return x_31;
+}
+}
+}
+else
+{
+uint8_t x_32; 
+lean_dec(x_7);
+lean_dec(x_4);
+lean_dec(x_3);
+x_32 = !lean_is_exclusive(x_10);
+if (x_32 == 0)
+{
+return x_10;
+}
+else
 {
 lean_object* x_33; lean_object* x_34; lean_object* x_35; 
-x_33 = lean_ctor_get(x_32, 0);
-lean_inc(x_33);
-x_34 = lean_ctor_get(x_32, 1);
+x_33 = lean_ctor_get(x_10, 0);
+x_34 = lean_ctor_get(x_10, 1);
 lean_inc(x_34);
-lean_dec(x_32);
-x_35 = l_Lean_Elab_Term_mkLambda(x_3, x_30, x_4, x_34);
-if (lean_obj_tag(x_35) == 0)
+lean_inc(x_33);
+lean_dec(x_10);
+x_35 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_35, 0, x_33);
+lean_ctor_set(x_35, 1, x_34);
+return x_35;
+}
+}
+}
+else
 {
 uint8_t x_36; 
-x_36 = !lean_is_exclusive(x_35);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+x_36 = !lean_is_exclusive(x_6);
 if (x_36 == 0)
 {
-lean_object* x_37; lean_object* x_38; 
-x_37 = lean_ctor_get(x_35, 0);
-x_38 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_38, 0, x_33);
-lean_ctor_set(x_38, 1, x_37);
-lean_ctor_set(x_35, 0, x_38);
-return x_35;
-}
-else
-{
-lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; 
-x_39 = lean_ctor_get(x_35, 0);
-x_40 = lean_ctor_get(x_35, 1);
-lean_inc(x_40);
-lean_inc(x_39);
-lean_dec(x_35);
-x_41 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_41, 0, x_33);
-lean_ctor_set(x_41, 1, x_39);
-x_42 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_42, 0, x_41);
-lean_ctor_set(x_42, 1, x_40);
-return x_42;
-}
-}
-else
-{
-uint8_t x_43; 
-lean_dec(x_33);
-x_43 = !lean_is_exclusive(x_35);
-if (x_43 == 0)
-{
-return x_35;
-}
-else
-{
-lean_object* x_44; lean_object* x_45; lean_object* x_46; 
-x_44 = lean_ctor_get(x_35, 0);
-x_45 = lean_ctor_get(x_35, 1);
-lean_inc(x_45);
-lean_inc(x_44);
-lean_dec(x_35);
-x_46 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_46, 0, x_44);
-lean_ctor_set(x_46, 1, x_45);
-return x_46;
-}
-}
-}
-else
-{
-uint8_t x_47; 
-lean_dec(x_30);
-lean_dec(x_4);
-lean_dec(x_3);
-x_47 = !lean_is_exclusive(x_32);
-if (x_47 == 0)
-{
-return x_32;
-}
-else
-{
-lean_object* x_48; lean_object* x_49; lean_object* x_50; 
-x_48 = lean_ctor_get(x_32, 0);
-x_49 = lean_ctor_get(x_32, 1);
-lean_inc(x_49);
-lean_inc(x_48);
-lean_dec(x_32);
-x_50 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_50, 0, x_48);
-lean_ctor_set(x_50, 1, x_49);
-return x_50;
-}
-}
-}
-else
-{
-uint8_t x_51; 
-lean_dec(x_7);
-lean_dec(x_4);
-lean_dec(x_3);
-x_51 = !lean_is_exclusive(x_29);
-if (x_51 == 0)
-{
-return x_29;
-}
-else
-{
-lean_object* x_52; lean_object* x_53; lean_object* x_54; 
-x_52 = lean_ctor_get(x_29, 0);
-x_53 = lean_ctor_get(x_29, 1);
-lean_inc(x_53);
-lean_inc(x_52);
-lean_dec(x_29);
-x_54 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_54, 0, x_52);
-lean_ctor_set(x_54, 1, x_53);
-return x_54;
-}
-}
-}
-else
-{
-uint8_t x_55; 
-lean_dec(x_9);
-lean_dec(x_7);
-lean_dec(x_4);
-lean_dec(x_3);
-lean_dec(x_2);
-x_55 = !lean_is_exclusive(x_11);
-if (x_55 == 0)
-{
-return x_11;
-}
-else
-{
-lean_object* x_56; lean_object* x_57; lean_object* x_58; 
-x_56 = lean_ctor_get(x_11, 0);
-x_57 = lean_ctor_get(x_11, 1);
-lean_inc(x_57);
-lean_inc(x_56);
-lean_dec(x_11);
-x_58 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_58, 0, x_56);
-lean_ctor_set(x_58, 1, x_57);
-return x_58;
-}
-}
-}
-else
-{
-uint8_t x_59; 
-lean_dec(x_4);
-lean_dec(x_3);
-lean_dec(x_2);
-x_59 = !lean_is_exclusive(x_6);
-if (x_59 == 0)
-{
 return x_6;
 }
 else
 {
-lean_object* x_60; lean_object* x_61; lean_object* x_62; 
-x_60 = lean_ctor_get(x_6, 0);
-x_61 = lean_ctor_get(x_6, 1);
-lean_inc(x_61);
-lean_inc(x_60);
+lean_object* x_37; lean_object* x_38; lean_object* x_39; 
+x_37 = lean_ctor_get(x_6, 0);
+x_38 = lean_ctor_get(x_6, 1);
+lean_inc(x_38);
+lean_inc(x_37);
 lean_dec(x_6);
-x_62 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_62, 0, x_60);
-lean_ctor_set(x_62, 1, x_61);
-return x_62;
+x_39 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_39, 0, x_37);
+lean_ctor_set(x_39, 1, x_38);
+return x_39;
 }
 }
 }

stage0/stdlib/Lean/Elab/BuiltinNotation.c

@@ -1904,6 +1904,8 @@ x_7 = lean_unsigned_to_nat(1u);
 x_8 = l_Lean_Syntax_getArg(x_1, x_7);
 x_9 = l_Lean_Syntax_getArgs(x_8);
 lean_dec(x_8);
+lean_inc(x_3);
+lean_inc(x_2);
 x_10 = l_Lean_Elab_Term_tryPostponeIfNoneOrMVar(x_2, x_3, x_4);
 if (lean_obj_tag(x_10) == 0)
 {
@@ -6392,6 +6394,8 @@ else
 {
 lean_object* x_9; 
 lean_dec(x_1);
+lean_inc(x_3);
+lean_inc(x_2);
 x_9 = l_Lean_Elab_Term_tryPostponeIfNoneOrMVar(x_2, x_3, x_4);
 if (lean_obj_tag(x_9) == 0)
 {

stage0/stdlib/Lean/Elab/Syntax.c

@@ -17538,6 +17538,8 @@ lean_object* l_Lean_Elab_Command_withExpectedType(lean_object* x_1, lean_object*
 _start:
 {
 lean_object* x_5; 
+lean_inc(x_3);
+lean_inc(x_1);
 x_5 = l_Lean_Elab_Term_tryPostponeIfNoneOrMVar(x_1, x_3, x_4);
 if (lean_obj_tag(x_5) == 0)
 {

stage0/stdlib/Lean/Elab/SyntheticMVars.c

@@ -1856,6 +1856,16 @@ x_48 = lean_ctor_get_uint8(x_6, sizeof(void*)*10 + 1);
 x_49 = lean_ctor_get_uint8(x_6, sizeof(void*)*10 + 2);
 x_50 = lean_ctor_get(x_6, 9);
 lean_inc(x_50);
+lean_inc(x_50);
+lean_inc(x_46);
+lean_inc(x_2);
+lean_inc(x_45);
+lean_inc(x_44);
+lean_inc(x_43);
+lean_inc(x_42);
+lean_inc(x_41);
+lean_inc(x_40);
+lean_inc(x_39);
 x_51 = lean_alloc_ctor(0, 10, 3);
 lean_ctor_set(x_51, 0, x_39);
 lean_ctor_set(x_51, 1, x_40);
@@ -1894,78 +1904,79 @@ uint8_t x_60; lean_object* x_61;
 x_60 = 1;
 lean_inc(x_51);
 lean_inc(x_59);
+lean_inc(x_4);
 x_61 = l___private_Lean_Elab_SyntheticMVars_1__resumeElabTerm(x_4, x_59, x_60, x_51, x_58);
 if (lean_obj_tag(x_61) == 0)
 {
-lean_object* x_62; lean_object* x_63; lean_object* x_64; 
+lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; 
 x_62 = lean_ctor_get(x_61, 0);
 lean_inc(x_62);
 x_63 = lean_ctor_get(x_61, 1);
 lean_inc(x_63);
 lean_dec(x_61);
-lean_inc(x_51);
-x_64 = l_Lean_Elab_Term_ensureHasType(x_59, x_62, x_51, x_63);
-if (lean_obj_tag(x_64) == 0)
+x_64 = l_Lean_Elab_replaceRef(x_4, x_50);
+lean_dec(x_50);
+lean_dec(x_4);
+x_65 = lean_alloc_ctor(0, 10, 3);
+lean_ctor_set(x_65, 0, x_39);
+lean_ctor_set(x_65, 1, x_40);
+lean_ctor_set(x_65, 2, x_41);
+lean_ctor_set(x_65, 3, x_42);
+lean_ctor_set(x_65, 4, x_43);
+lean_ctor_set(x_65, 5, x_44);
+lean_ctor_set(x_65, 6, x_45);
+lean_ctor_set(x_65, 7, x_2);
+lean_ctor_set(x_65, 8, x_46);
+lean_ctor_set(x_65, 9, x_64);
+lean_ctor_set_uint8(x_65, sizeof(void*)*10, x_47);
+lean_ctor_set_uint8(x_65, sizeof(void*)*10 + 1, x_48);
+lean_ctor_set_uint8(x_65, sizeof(void*)*10 + 2, x_49);
+x_66 = l_Lean_Elab_Term_ensureHasType(x_59, x_62, x_65, x_63);
+if (lean_obj_tag(x_66) == 0)
 {
-lean_object* x_65; lean_object* x_66; lean_object* x_67; uint8_t x_68; 
+lean_object* x_67; lean_object* x_68; lean_object* x_69; uint8_t x_70; 
 lean_dec(x_6);
 lean_dec(x_5);
-x_65 = lean_ctor_get(x_64, 0);
-lean_inc(x_65);
-x_66 = lean_ctor_get(x_64, 1);
-lean_inc(x_66);
-lean_dec(x_64);
-x_67 = l_Lean_Elab_Term_assignExprMVar(x_3, x_65, x_51, x_66);
+x_67 = lean_ctor_get(x_66, 0);
+lean_inc(x_67);
+x_68 = lean_ctor_get(x_66, 1);
+lean_inc(x_68);
+lean_dec(x_66);
+x_69 = l_Lean_Elab_Term_assignExprMVar(x_3, x_67, x_51, x_68);
 lean_dec(x_51);
-x_68 = !lean_is_exclusive(x_67);
-if (x_68 == 0)
+x_70 = !lean_is_exclusive(x_69);
+if (x_70 == 0)
 {
-lean_object* x_69; lean_object* x_70; 
-x_69 = lean_ctor_get(x_67, 0);
-lean_dec(x_69);
-x_70 = lean_box(x_60);
-lean_ctor_set(x_67, 0, x_70);
-return x_67;
-}
-else
-{
-lean_object* x_71; lean_object* x_72; lean_object* x_73; 
-x_71 = lean_ctor_get(x_67, 1);
-lean_inc(x_71);
-lean_dec(x_67);
+lean_object* x_71; lean_object* x_72; 
+x_71 = lean_ctor_get(x_69, 0);
+lean_dec(x_71);
 x_72 = lean_box(x_60);
-x_73 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_73, 0, x_72);
-lean_ctor_set(x_73, 1, x_71);
-return x_73;
-}
+lean_ctor_set(x_69, 0, x_72);
+return x_69;
 }
 else
 {
-lean_object* x_74; lean_object* x_75; 
-lean_dec(x_51);
-lean_dec(x_3);
-x_74 = lean_ctor_get(x_64, 0);
-lean_inc(x_74);
-x_75 = lean_ctor_get(x_64, 1);
-lean_inc(x_75);
-lean_dec(x_64);
-x_8 = x_74;
-x_9 = x_75;
-goto block_38;
+lean_object* x_73; lean_object* x_74; lean_object* x_75; 
+x_73 = lean_ctor_get(x_69, 1);
+lean_inc(x_73);
+lean_dec(x_69);
+x_74 = lean_box(x_60);
+x_75 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_75, 0, x_74);
+lean_ctor_set(x_75, 1, x_73);
+return x_75;
 }
 }
 else
 {
 lean_object* x_76; lean_object* x_77; 
-lean_dec(x_59);
 lean_dec(x_51);
 lean_dec(x_3);
-x_76 = lean_ctor_get(x_61, 0);
+x_76 = lean_ctor_get(x_66, 0);
 lean_inc(x_76);
-x_77 = lean_ctor_get(x_61, 1);
+x_77 = lean_ctor_get(x_66, 1);
 lean_inc(x_77);
-lean_dec(x_61);
+lean_dec(x_66);
 x_8 = x_76;
 x_9 = x_77;
 goto block_38;
@@ -1973,86 +1984,141 @@ goto block_38;
 }
 else
 {
-uint8_t x_78; lean_object* x_79; 
-x_78 = 0;
-lean_inc(x_51);
-lean_inc(x_59);
-x_79 = l___private_Lean_Elab_SyntheticMVars_1__resumeElabTerm(x_4, x_59, x_78, x_51, x_58);
-if (lean_obj_tag(x_79) == 0)
-{
-lean_object* x_80; lean_object* x_81; lean_object* x_82; 
-x_80 = lean_ctor_get(x_79, 0);
-lean_inc(x_80);
-x_81 = lean_ctor_get(x_79, 1);
-lean_inc(x_81);
-lean_dec(x_79);
-lean_inc(x_51);
-x_82 = l_Lean_Elab_Term_ensureHasType(x_59, x_80, x_51, x_81);
-if (lean_obj_tag(x_82) == 0)
-{
-lean_object* x_83; lean_object* x_84; lean_object* x_85; uint8_t x_86; 
-lean_dec(x_6);
-lean_dec(x_5);
-x_83 = lean_ctor_get(x_82, 0);
-lean_inc(x_83);
-x_84 = lean_ctor_get(x_82, 1);
-lean_inc(x_84);
-lean_dec(x_82);
-x_85 = l_Lean_Elab_Term_assignExprMVar(x_3, x_83, x_51, x_84);
-lean_dec(x_51);
-x_86 = !lean_is_exclusive(x_85);
-if (x_86 == 0)
-{
-lean_object* x_87; uint8_t x_88; lean_object* x_89; 
-x_87 = lean_ctor_get(x_85, 0);
-lean_dec(x_87);
-x_88 = 1;
-x_89 = lean_box(x_88);
-lean_ctor_set(x_85, 0, x_89);
-return x_85;
-}
-else
-{
-lean_object* x_90; uint8_t x_91; lean_object* x_92; lean_object* x_93; 
-x_90 = lean_ctor_get(x_85, 1);
-lean_inc(x_90);
-lean_dec(x_85);
-x_91 = 1;
-x_92 = lean_box(x_91);
-x_93 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_93, 0, x_92);
-lean_ctor_set(x_93, 1, x_90);
-return x_93;
-}
-}
-else
-{
-lean_object* x_94; lean_object* x_95; 
+lean_object* x_78; lean_object* x_79; 
+lean_dec(x_59);
 lean_dec(x_51);
+lean_dec(x_50);
+lean_dec(x_46);
+lean_dec(x_45);
+lean_dec(x_44);
+lean_dec(x_43);
+lean_dec(x_42);
+lean_dec(x_41);
+lean_dec(x_40);
+lean_dec(x_39);
+lean_dec(x_4);
 lean_dec(x_3);
-x_94 = lean_ctor_get(x_82, 0);
-lean_inc(x_94);
-x_95 = lean_ctor_get(x_82, 1);
-lean_inc(x_95);
-lean_dec(x_82);
-x_8 = x_94;
-x_9 = x_95;
+lean_dec(x_2);
+x_78 = lean_ctor_get(x_61, 0);
+lean_inc(x_78);
+x_79 = lean_ctor_get(x_61, 1);
+lean_inc(x_79);
+lean_dec(x_61);
+x_8 = x_78;
+x_9 = x_79;
 goto block_38;
 }
 }
 else
 {
-lean_object* x_96; lean_object* x_97; 
-lean_dec(x_59);
+uint8_t x_80; lean_object* x_81; 
+x_80 = 0;
+lean_inc(x_51);
+lean_inc(x_59);
+lean_inc(x_4);
+x_81 = l___private_Lean_Elab_SyntheticMVars_1__resumeElabTerm(x_4, x_59, x_80, x_51, x_58);
+if (lean_obj_tag(x_81) == 0)
+{
+lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; 
+x_82 = lean_ctor_get(x_81, 0);
+lean_inc(x_82);
+x_83 = lean_ctor_get(x_81, 1);
+lean_inc(x_83);
+lean_dec(x_81);
+x_84 = l_Lean_Elab_replaceRef(x_4, x_50);
+lean_dec(x_50);
+lean_dec(x_4);
+x_85 = lean_alloc_ctor(0, 10, 3);
+lean_ctor_set(x_85, 0, x_39);
+lean_ctor_set(x_85, 1, x_40);
+lean_ctor_set(x_85, 2, x_41);
+lean_ctor_set(x_85, 3, x_42);
+lean_ctor_set(x_85, 4, x_43);
+lean_ctor_set(x_85, 5, x_44);
+lean_ctor_set(x_85, 6, x_45);
+lean_ctor_set(x_85, 7, x_2);
+lean_ctor_set(x_85, 8, x_46);
+lean_ctor_set(x_85, 9, x_84);
+lean_ctor_set_uint8(x_85, sizeof(void*)*10, x_47);
+lean_ctor_set_uint8(x_85, sizeof(void*)*10 + 1, x_48);
+lean_ctor_set_uint8(x_85, sizeof(void*)*10 + 2, x_49);
+x_86 = l_Lean_Elab_Term_ensureHasType(x_59, x_82, x_85, x_83);
+if (lean_obj_tag(x_86) == 0)
+{
+lean_object* x_87; lean_object* x_88; lean_object* x_89; uint8_t x_90; 
+lean_dec(x_6);
+lean_dec(x_5);
+x_87 = lean_ctor_get(x_86, 0);
+lean_inc(x_87);
+x_88 = lean_ctor_get(x_86, 1);
+lean_inc(x_88);
+lean_dec(x_86);
+x_89 = l_Lean_Elab_Term_assignExprMVar(x_3, x_87, x_51, x_88);
+lean_dec(x_51);
+x_90 = !lean_is_exclusive(x_89);
+if (x_90 == 0)
+{
+lean_object* x_91; uint8_t x_92; lean_object* x_93; 
+x_91 = lean_ctor_get(x_89, 0);
+lean_dec(x_91);
+x_92 = 1;
+x_93 = lean_box(x_92);
+lean_ctor_set(x_89, 0, x_93);
+return x_89;
+}
+else
+{
+lean_object* x_94; uint8_t x_95; lean_object* x_96; lean_object* x_97; 
+x_94 = lean_ctor_get(x_89, 1);
+lean_inc(x_94);
+lean_dec(x_89);
+x_95 = 1;
+x_96 = lean_box(x_95);
+x_97 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_97, 0, x_96);
+lean_ctor_set(x_97, 1, x_94);
+return x_97;
+}
+}
+else
+{
+lean_object* x_98; lean_object* x_99; 
 lean_dec(x_51);
 lean_dec(x_3);
-x_96 = lean_ctor_get(x_79, 0);
-lean_inc(x_96);
-x_97 = lean_ctor_get(x_79, 1);
-lean_inc(x_97);
-lean_dec(x_79);
-x_8 = x_96;
-x_9 = x_97;
+x_98 = lean_ctor_get(x_86, 0);
+lean_inc(x_98);
+x_99 = lean_ctor_get(x_86, 1);
+lean_inc(x_99);
+lean_dec(x_86);
+x_8 = x_98;
+x_9 = x_99;
+goto block_38;
+}
+}
+else
+{
+lean_object* x_100; lean_object* x_101; 
+lean_dec(x_59);
+lean_dec(x_51);
+lean_dec(x_50);
+lean_dec(x_46);
+lean_dec(x_45);
+lean_dec(x_44);
+lean_dec(x_43);
+lean_dec(x_42);
+lean_dec(x_41);
+lean_dec(x_40);
+lean_dec(x_39);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+x_100 = lean_ctor_get(x_81, 0);
+lean_inc(x_100);
+x_101 = lean_ctor_get(x_81, 1);
+lean_inc(x_101);
+lean_dec(x_81);
+x_8 = x_100;
+x_9 = x_101;
 goto block_38;
 }
 }

stage0/stdlib/Lean/Elab/Term.c

@@ -286,6 +286,7 @@ lean_object* l_Lean_Elab_Term_monadLog___closed__1;
 lean_object* l___private_Lean_Elab_Term_18__mkPairsAux___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_isCharLit_x3f(lean_object*);
 lean_object* l_Array_isEqvAux___main___at_Lean_Elab_Term_withMVarContext___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Elab_Term_elabTermEnsuringType(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_fget(lean_object*, lean_object*);
 lean_object* l_Std_PersistentArray_foldlM___at___private_Lean_Elab_Term_3__fromMetaState___spec__1___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___closed__5;
@@ -648,7 +649,6 @@ uint8_t l___private_Lean_Elab_Term_14__isLambdaWithImplicit(lean_object*);
 extern lean_object* l_Lean_EnvExtension_setState___closed__1;
 lean_object* l_Lean_Elab_Term_liftLevelM___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_modifyEnv(lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Elab_Term_tryPostponeIfMVar___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_ReaderT_lift___at_Lean_Elab_Term_Lean_Elab_MonadMacroAdapter___spec__1(lean_object*);
 lean_object* l_Lean_Elab_Term_whnfCore(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_monadLog___lambda__4___boxed(lean_object*, lean_object*, lean_object*);
@@ -833,7 +833,6 @@ lean_object* l_Lean_Elab_Term_withReducible___rarg(lean_object*, lean_object*, l
 lean_object* l_Lean_Elab_Term_instantiateLevelMVars(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_ensureHasTypeAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_tryLiftAndCoe___closed__5;
-lean_object* l_Lean_Elab_Term_tryPostponeIfNoneOrMVar___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* lean_uint32_to_nat(uint32_t);
 lean_object* l_Lean_Elab_Term_throwTypeMismatchError___rarg___closed__1;
 lean_object* l___private_Lean_Elab_Term_17__elabOptLevel(lean_object*, lean_object*, lean_object*);
@@ -18026,6 +18025,8 @@ lean_dec(x_4);
 if (x_5 == 0)
 {
 lean_object* x_6; lean_object* x_7; 
+lean_dec(x_2);
+lean_dec(x_1);
 x_6 = lean_box(0);
 x_7 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_7, 0, x_6);
@@ -18034,20 +18035,67 @@ return x_7;
 }
 else
 {
-lean_object* x_8; 
-x_8 = l_Lean_Elab_Term_tryPostpone(x_2, x_3);
+lean_object* x_8; uint8_t x_9; 
+lean_inc(x_2);
+x_8 = l_Lean_Elab_Term_instantiateMVars(x_1, x_2, x_3);
+x_9 = !lean_is_exclusive(x_8);
+if (x_9 == 0)
+{
+lean_object* x_10; lean_object* x_11; lean_object* x_12; uint8_t x_13; 
+x_10 = lean_ctor_get(x_8, 0);
+x_11 = lean_ctor_get(x_8, 1);
+x_12 = l_Lean_Expr_getAppFn___main(x_10);
+lean_dec(x_10);
+x_13 = l_Lean_Expr_isMVar(x_12);
+lean_dec(x_12);
+if (x_13 == 0)
+{
+lean_object* x_14; 
+lean_dec(x_2);
+x_14 = lean_box(0);
+lean_ctor_set(x_8, 0, x_14);
 return x_8;
 }
-}
-}
-lean_object* l_Lean_Elab_Term_tryPostponeIfMVar___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
-_start:
+else
 {
-lean_object* x_4; 
-x_4 = l_Lean_Elab_Term_tryPostponeIfMVar(x_1, x_2, x_3);
+lean_object* x_15; 
+lean_free_object(x_8);
+x_15 = l_Lean_Elab_Term_tryPostpone(x_2, x_11);
 lean_dec(x_2);
-lean_dec(x_1);
-return x_4;
+return x_15;
+}
+}
+else
+{
+lean_object* x_16; lean_object* x_17; lean_object* x_18; uint8_t x_19; 
+x_16 = lean_ctor_get(x_8, 0);
+x_17 = lean_ctor_get(x_8, 1);
+lean_inc(x_17);
+lean_inc(x_16);
+lean_dec(x_8);
+x_18 = l_Lean_Expr_getAppFn___main(x_16);
+lean_dec(x_16);
+x_19 = l_Lean_Expr_isMVar(x_18);
+lean_dec(x_18);
+if (x_19 == 0)
+{
+lean_object* x_20; lean_object* x_21; 
+lean_dec(x_2);
+x_20 = lean_box(0);
+x_21 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_21, 0, x_20);
+lean_ctor_set(x_21, 1, x_17);
+return x_21;
+}
+else
+{
+lean_object* x_22; 
+x_22 = l_Lean_Elab_Term_tryPostpone(x_2, x_17);
+lean_dec(x_2);
+return x_22;
+}
+}
+}
 }
 }
 lean_object* l_Lean_Elab_Term_tryPostponeIfNoneOrMVar(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
@@ -18057,27 +18105,20 @@ if (lean_obj_tag(x_1) == 0)
 {
 lean_object* x_4; 
 x_4 = l_Lean_Elab_Term_tryPostpone(x_2, x_3);
+lean_dec(x_2);
 return x_4;
 }
 else
 {
 lean_object* x_5; lean_object* x_6; 
 x_5 = lean_ctor_get(x_1, 0);
+lean_inc(x_5);
+lean_dec(x_1);
 x_6 = l_Lean_Elab_Term_tryPostponeIfMVar(x_5, x_2, x_3);
 return x_6;
 }
 }
 }
-lean_object* l_Lean_Elab_Term_tryPostponeIfNoneOrMVar___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
-_start:
-{
-lean_object* x_4; 
-x_4 = l_Lean_Elab_Term_tryPostponeIfNoneOrMVar(x_1, x_2, x_3);
-lean_dec(x_2);
-lean_dec(x_1);
-return x_4;
-}
-}
 lean_object* _init_l___private_Lean_Elab_Term_10__postponeElabTerm___closed__1() {
 _start:
 {
@@ -22425,6 +22466,110 @@ x_7 = l_Lean_Elab_Term_elabTerm(x_1, x_2, x_6, x_4, x_5);
 return x_7;
 }
 }
+lean_object* l_Lean_Elab_Term_elabTermEnsuringType(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+uint8_t x_5; lean_object* x_6; 
+x_5 = 1;
+lean_inc(x_3);
+lean_inc(x_2);
+lean_inc(x_1);
+x_6 = l_Lean_Elab_Term_elabTerm(x_1, x_2, x_5, x_3, x_4);
+if (lean_obj_tag(x_6) == 0)
+{
+lean_object* x_7; lean_object* x_8; uint8_t x_9; 
+x_7 = lean_ctor_get(x_6, 0);
+lean_inc(x_7);
+x_8 = lean_ctor_get(x_6, 1);
+lean_inc(x_8);
+lean_dec(x_6);
+x_9 = !lean_is_exclusive(x_3);
+if (x_9 == 0)
+{
+lean_object* x_10; lean_object* x_11; lean_object* x_12; 
+x_10 = lean_ctor_get(x_3, 9);
+x_11 = l_Lean_Elab_replaceRef(x_1, x_10);
+lean_dec(x_10);
+lean_dec(x_1);
+lean_ctor_set(x_3, 9, x_11);
+x_12 = l_Lean_Elab_Term_ensureHasType(x_2, x_7, x_3, x_8);
+return x_12;
+}
+else
+{
+lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; uint8_t x_22; uint8_t x_23; uint8_t x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; 
+x_13 = lean_ctor_get(x_3, 0);
+x_14 = lean_ctor_get(x_3, 1);
+x_15 = lean_ctor_get(x_3, 2);
+x_16 = lean_ctor_get(x_3, 3);
+x_17 = lean_ctor_get(x_3, 4);
+x_18 = lean_ctor_get(x_3, 5);
+x_19 = lean_ctor_get(x_3, 6);
+x_20 = lean_ctor_get(x_3, 7);
+x_21 = lean_ctor_get(x_3, 8);
+x_22 = lean_ctor_get_uint8(x_3, sizeof(void*)*10);
+x_23 = lean_ctor_get_uint8(x_3, sizeof(void*)*10 + 1);
+x_24 = lean_ctor_get_uint8(x_3, sizeof(void*)*10 + 2);
+x_25 = lean_ctor_get(x_3, 9);
+lean_inc(x_25);
+lean_inc(x_21);
+lean_inc(x_20);
+lean_inc(x_19);
+lean_inc(x_18);
+lean_inc(x_17);
+lean_inc(x_16);
+lean_inc(x_15);
+lean_inc(x_14);
+lean_inc(x_13);
+lean_dec(x_3);
+x_26 = l_Lean_Elab_replaceRef(x_1, x_25);
+lean_dec(x_25);
+lean_dec(x_1);
+x_27 = lean_alloc_ctor(0, 10, 3);
+lean_ctor_set(x_27, 0, x_13);
+lean_ctor_set(x_27, 1, x_14);
+lean_ctor_set(x_27, 2, x_15);
+lean_ctor_set(x_27, 3, x_16);
+lean_ctor_set(x_27, 4, x_17);
+lean_ctor_set(x_27, 5, x_18);
+lean_ctor_set(x_27, 6, x_19);
+lean_ctor_set(x_27, 7, x_20);
+lean_ctor_set(x_27, 8, x_21);
+lean_ctor_set(x_27, 9, x_26);
+lean_ctor_set_uint8(x_27, sizeof(void*)*10, x_22);
+lean_ctor_set_uint8(x_27, sizeof(void*)*10 + 1, x_23);
+lean_ctor_set_uint8(x_27, sizeof(void*)*10 + 2, x_24);
+x_28 = l_Lean_Elab_Term_ensureHasType(x_2, x_7, x_27, x_8);
+return x_28;
+}
+}
+else
+{
+uint8_t x_29; 
+lean_dec(x_3);
+lean_dec(x_2);
+lean_dec(x_1);
+x_29 = !lean_is_exclusive(x_6);
+if (x_29 == 0)
+{
+return x_6;
+}
+else
+{
+lean_object* x_30; lean_object* x_31; lean_object* x_32; 
+x_30 = lean_ctor_get(x_6, 0);
+x_31 = lean_ctor_get(x_6, 1);
+lean_inc(x_31);
+lean_inc(x_30);
+lean_dec(x_6);
+x_32 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_32, 0, x_30);
+lean_ctor_set(x_32, 1, x_31);
+return x_32;
+}
+}
+}
+}
 lean_object* l_Lean_Elab_Term_elabTermWithoutImplicitLambdas(lean_object* x_1, lean_object* x_2, uint8_t x_3, lean_object* x_4, lean_object* x_5) {
 _start:
 {

stage0/stdlib/Lean/Parser/Tactic.c

@@ -144,7 +144,6 @@ lean_object* l_Lean_Parser_Tactic_apply___closed__4;
 lean_object* l_Lean_Parser_Tactic_allGoals___elambda__1___closed__6;
 lean_object* l_Lean_Parser_Tactic_exact___elambda__1___closed__6;
 extern lean_object* l_Lean_Parser_darrow;
-extern lean_object* l_Lean_Parser_Term_le_parenthesizer___closed__2;
 extern lean_object* l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__1;
 lean_object* l_Lean_Parser_Tactic_inductionAlt___closed__4;
 lean_object* l_Lean_Parser_Tactic_inductionAlt;
@@ -728,6 +727,7 @@ lean_object* l_Lean_Parser_Tactic_cases_parenthesizer___closed__3;
 extern lean_object* l_Lean_Parser_Term_namedHole_parenthesizer___closed__2;
 lean_object* l_Lean_Parser_Tactic_underscore_parenthesizer___rarg___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Tactic_inductionAlts___closed__1;
+lean_object* l_Lean_Parser_Tactic_generalize_parenthesizer___closed__7;
 lean_object* l___regBuiltin_Lean_Parser_Tactic_clear_parenthesizer(lean_object*);
 lean_object* l_Lean_Parser_Tactic_skip_parenthesizer___closed__2;
 lean_object* l_Lean_Parser_Tactic_cases_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -803,6 +803,7 @@ lean_object* l_Lean_Parser_Tactic_paren___closed__7;
 extern lean_object* l_Lean_Parser_Term_tacticBlock___elambda__1___closed__14;
 lean_object* l_Lean_Parser_Tactic_clear_parenthesizer___closed__1;
 lean_object* l_Lean_Parser_Tactic_allGoals___elambda__1___closed__4;
+lean_object* l_Lean_Parser_termParser_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t lean_string_dec_eq(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Tactic_withAlts___closed__3;
 lean_object* l_Lean_Parser_Tactic_majorPremise;
@@ -7851,21 +7852,19 @@ return x_2;
 lean_object* _init_l_Lean_Parser_Tactic_generalize_parenthesizer___closed__3() {
 _start:
 {
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Term_le_parenthesizer___closed__2;
-x_2 = l_Lean_Parser_Term_namedHole_parenthesizer___closed__2;
-x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 6, 2);
-lean_closure_set(x_3, 0, x_1);
-lean_closure_set(x_3, 1, x_2);
-return x_3;
+lean_object* x_1; lean_object* x_2; 
+x_1 = lean_unsigned_to_nat(51u);
+x_2 = lean_alloc_closure((void*)(l_Lean_Parser_termParser_parenthesizer), 5, 1);
+lean_closure_set(x_2, 0, x_1);
+return x_2;
 }
 }
 lean_object* _init_l_Lean_Parser_Tactic_generalize_parenthesizer___closed__4() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__2;
-x_2 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__3;
+x_1 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__3;
+x_2 = l_Lean_Parser_Term_namedHole_parenthesizer___closed__2;
 x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 6, 2);
 lean_closure_set(x_3, 0, x_1);
 lean_closure_set(x_3, 1, x_2);
@@ -7876,7 +7875,7 @@ lean_object* _init_l_Lean_Parser_Tactic_generalize_parenthesizer___closed__5() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_PrettyPrinter_Parenthesizer_compileParenthesizerDescr___main___closed__2;
+x_1 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__2;
 x_2 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__4;
 x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 6, 2);
 lean_closure_set(x_3, 0, x_1);
@@ -7887,10 +7886,22 @@ return x_3;
 lean_object* _init_l_Lean_Parser_Tactic_generalize_parenthesizer___closed__6() {
 _start:
 {
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_PrettyPrinter_Parenthesizer_compileParenthesizerDescr___main___closed__2;
+x_2 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__5;
+x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer), 6, 2);
+lean_closure_set(x_3, 0, x_1);
+lean_closure_set(x_3, 1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_Parser_Tactic_generalize_parenthesizer___closed__7() {
+_start:
+{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_1 = l_Lean_Parser_Tactic_generalize___elambda__1___closed__2;
 x_2 = lean_unsigned_to_nat(1024u);
-x_3 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__5;
+x_3 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__6;
 x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer), 7, 3);
 lean_closure_set(x_4, 0, x_1);
 lean_closure_set(x_4, 1, x_2);
@@ -7903,7 +7914,7 @@ _start:
 {
 lean_object* x_5; lean_object* x_6; lean_object* x_7; 
 x_5 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__1;
-x_6 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__6;
+x_6 = l_Lean_Parser_Tactic_generalize_parenthesizer___closed__7;
 x_7 = l_Lean_PrettyPrinter_Parenthesizer_orelse_parenthesizer(x_5, x_6, x_1, x_2, x_3, x_4);
 return x_7;
 }
@@ -16409,6 +16420,8 @@ l_Lean_Parser_Tactic_generalize_parenthesizer___closed__5 = _init_l_Lean_Parser_
 lean_mark_persistent(l_Lean_Parser_Tactic_generalize_parenthesizer___closed__5);
 l_Lean_Parser_Tactic_generalize_parenthesizer___closed__6 = _init_l_Lean_Parser_Tactic_generalize_parenthesizer___closed__6();
 lean_mark_persistent(l_Lean_Parser_Tactic_generalize_parenthesizer___closed__6);
+l_Lean_Parser_Tactic_generalize_parenthesizer___closed__7 = _init_l_Lean_Parser_Tactic_generalize_parenthesizer___closed__7();
+lean_mark_persistent(l_Lean_Parser_Tactic_generalize_parenthesizer___closed__7);
 l___regBuiltin_Lean_Parser_Tactic_generalize_parenthesizer___closed__1 = _init_l___regBuiltin_Lean_Parser_Tactic_generalize_parenthesizer___closed__1();
 lean_mark_persistent(l___regBuiltin_Lean_Parser_Tactic_generalize_parenthesizer___closed__1);
 res = l___regBuiltin_Lean_Parser_Tactic_generalize_parenthesizer(lean_io_mk_world());