chore: update stage0

stage0/src/Init/Core.lean

@@ -89,6 +89,12 @@ class ForIn (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v))
 
 export ForIn (forIn)
 
+class ForIn' (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v)) [d : outParam $ Membership α ρ] where
+  forIn' {β} [Monad m] (x : ρ) (b : β) (f : (a : α) → a ∈ x → β → m (ForInStep β)) : m β
+
+export ForIn' (forIn')
+
+
 /- Auxiliary type used to compile `do` notation. -/
 inductive DoResultPRBC (α β σ : Type u) where
   | «pure»     : α → σ → DoResultPRBC α β σ

stage0/src/Init/Data/List/Basic.lean

@@ -81,6 +81,11 @@ theorem append_assoc (as bs cs : List α) : (as ++ bs) ++ cs = as ++ (bs ++ cs)
   | nil => rfl
   | cons a as ih => simp [ih]
 
+theorem append_cons (as : List α) (b : α) (bs : List α) : as ++ b :: bs = as ++ [b] ++ bs := by
+  induction as with
+  | nil => simp
+  | cons a as ih => simp [ih]
+
 instance : EmptyCollection (List α) := ⟨List.nil⟩
 
 protected def erase {α} [BEq α] : List α → α → List α
@@ -236,6 +241,18 @@ theorem elem_eq_true_of_mem [DecidableEq α] {a : α} {as : List α} (h : a ∈
 instance [DecidableEq α] (a : α) (as : List α) : Decidable (a ∈ as) :=
   decidable_of_decidable_of_iff (Iff.intro mem_of_elem_eq_true elem_eq_true_of_mem)
 
+theorem mem_append_of_mem_left {a : α} {as : List α} (bs : List α) : a ∈ as → a ∈ as ++ bs := by
+  intro h
+  induction h with
+  | head => apply Mem.head
+  | tail => apply Mem.tail; assumption
+
+theorem mem_append_of_mem_right {b : α} {bs : List α} (as : List α) : b ∈ bs → b ∈ as ++ bs := by
+  intro h
+  induction as with
+  | nil  => simp [h]
+  | cons => apply Mem.tail; assumption
+
 def eraseDupsAux {α} [BEq α] : List α → List α → List α
   | [],    bs => bs.reverse
   | a::as, bs => match bs.elem a with

stage0/src/Init/Data/List/Control.lean

@@ -158,6 +158,24 @@ instance : ForIn m (List α) α where
     : forIn (a::as) b f = f a b >>= fun | ForInStep.done b => pure b | ForInStep.yield b => forIn as b f :=
   rfl
 
+@[inline] protected def forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : List α) (init : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β :=
+  let rec @[specialize] loop : (as' : List α) → (b : β) → Exists (fun bs => bs ++ as' = as) → m β
+    | [], b, _    => pure b
+    | a::as', b, h => do
+      have : a ∈ as := by
+        have ⟨bs, h⟩ := h
+        subst h
+        exact mem_append_of_mem_right _ (Mem.head ..)
+      match (← f a this b) with
+      | ForInStep.done b  => pure b
+      | ForInStep.yield b =>
+        have : Exists (fun bs => bs ++ as' = as) := have ⟨bs, h⟩ := h; ⟨bs ++ [a], by rw [← h, append_cons bs a as']⟩
+        loop as' b this
+  loop as init ⟨[], rfl⟩
+
+instance : ForIn' m (List α) α where
+  forIn' := List.forIn'
+
 instance : ForM m (List α) α where
   forM := List.forM
 

stage0/src/Lean/Parser/Term.lean

@@ -233,6 +233,7 @@ def matchAltsWhereDecls := leading_parser matchAlts >> optional whereDecls
 @[builtinTermParser] def binop_lazy  := leading_parser "binop_lazy% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
 
 @[builtinTermParser] def forInMacro := leading_parser "for_in% " >> termParser maxPrec >> termParser maxPrec >> termParser maxPrec
+@[builtinTermParser] def forInMacro' := leading_parser "for_in'% " >> termParser maxPrec >> termParser maxPrec >> termParser maxPrec
 
 @[builtinTermParser] def typeOf             := leading_parser "type_of% " >> termParser maxPrec
 @[builtinTermParser] def ensureTypeOf       := leading_parser "ensure_type_of% " >> termParser maxPrec >> strLit >> termParser

stage0/stdlib/Init/Data/List/Control.c

@@ -24,6 +24,7 @@ LEAN_EXPORT lean_object* l_List_firstM___rarg(lean_object*, lean_object*, lean_o
 LEAN_EXPORT lean_object* l_List_anyM___rarg___lambda__1(lean_object*, lean_object*, lean_object*, uint8_t);
 LEAN_EXPORT lean_object* l_List_filterM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_List_allM(lean_object*);
+LEAN_EXPORT lean_object* l_List_forIn_x27_loop___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_List_forIn(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_List_mapM(lean_object*);
 LEAN_EXPORT lean_object* l_List_foldlM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -32,6 +33,9 @@ LEAN_EXPORT lean_object* l_List_anyM(lean_object*);
 LEAN_EXPORT lean_object* l_List_allM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_List_mapA___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_List_forIn_loop(lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_List_forIn_x27___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_List_instForIn_x27ListInstMembershipList(lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_List_forIn_x27_loop(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_List_mapM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_List_allM___rarg___lambda__1(lean_object*, lean_object*, lean_object*, uint8_t);
 LEAN_EXPORT lean_object* l_List_findSomeM_x3f___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -41,6 +45,7 @@ LEAN_EXPORT lean_object* l_List_findM_x3f___rarg(lean_object*, lean_object*, lea
 LEAN_EXPORT lean_object* l_List_forIn_loop___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_List_forA___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_List_forA___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_List_forIn_x27(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_List_allM___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_List_filterAuxM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_List_filterMapM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -52,6 +57,7 @@ LEAN_EXPORT lean_object* l_List_forIn_loop___rarg(lean_object*, lean_object*, le
 LEAN_EXPORT lean_object* l_List_instForInList___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_List_filterM___rarg___lambda__1(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_List_anyM___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_List_instForIn_x27ListInstMembershipList___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_List_firstM(lean_object*);
 LEAN_EXPORT lean_object* l_List_instForMList(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_List_filterMapM_loop(lean_object*);
@@ -73,6 +79,7 @@ LEAN_EXPORT lean_object* l_List_findM_x3f(lean_object*);
 LEAN_EXPORT lean_object* l_List_forM(lean_object*);
 LEAN_EXPORT lean_object* l_List_foldrM(lean_object*);
 LEAN_EXPORT lean_object* l_List_findM_x3f___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_List_forIn_x27_loop___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_List_forM___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_List_mapA___rarg___lambda__1(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_List_mapM___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
@@ -1164,6 +1171,119 @@ x_4 = lean_alloc_closure((void*)(l_List_instForInList___rarg), 4, 0);
 return x_4;
 }
 }
+LEAN_EXPORT lean_object* l_List_forIn_x27_loop___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+_start:
+{
+if (lean_obj_tag(x_5) == 0)
+{
+lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; 
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+x_6 = lean_ctor_get(x_5, 0);
+lean_inc(x_6);
+lean_dec(x_5);
+x_7 = lean_ctor_get(x_1, 0);
+lean_inc(x_7);
+lean_dec(x_1);
+x_8 = lean_ctor_get(x_7, 1);
+lean_inc(x_8);
+lean_dec(x_7);
+x_9 = lean_apply_2(x_8, lean_box(0), x_6);
+return x_9;
+}
+else
+{
+lean_object* x_10; lean_object* x_11; 
+x_10 = lean_ctor_get(x_5, 0);
+lean_inc(x_10);
+lean_dec(x_5);
+x_11 = l_List_forIn_x27_loop___rarg(x_1, x_2, x_3, x_4, x_10, lean_box(0));
+return x_11;
+}
+}
+}
+LEAN_EXPORT lean_object* l_List_forIn_x27_loop___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
+_start:
+{
+if (lean_obj_tag(x_4) == 0)
+{
+lean_object* x_7; lean_object* x_8; lean_object* x_9; 
+lean_dec(x_3);
+lean_dec(x_2);
+x_7 = lean_ctor_get(x_1, 0);
+lean_inc(x_7);
+lean_dec(x_1);
+x_8 = lean_ctor_get(x_7, 1);
+lean_inc(x_8);
+lean_dec(x_7);
+x_9 = lean_apply_2(x_8, lean_box(0), x_5);
+return x_9;
+}
+else
+{
+lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; 
+x_10 = lean_ctor_get(x_4, 0);
+lean_inc(x_10);
+x_11 = lean_ctor_get(x_4, 1);
+lean_inc(x_11);
+lean_dec(x_4);
+x_12 = lean_ctor_get(x_1, 1);
+lean_inc(x_12);
+lean_inc(x_3);
+x_13 = lean_apply_3(x_3, x_10, lean_box(0), x_5);
+x_14 = lean_alloc_closure((void*)(l_List_forIn_x27_loop___rarg___lambda__1), 5, 4);
+lean_closure_set(x_14, 0, x_1);
+lean_closure_set(x_14, 1, x_2);
+lean_closure_set(x_14, 2, x_3);
+lean_closure_set(x_14, 3, x_11);
+x_15 = lean_apply_4(x_12, lean_box(0), lean_box(0), x_13, x_14);
+return x_15;
+}
+}
+}
+LEAN_EXPORT lean_object* l_List_forIn_x27_loop(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = lean_alloc_closure((void*)(l_List_forIn_x27_loop___rarg), 6, 0);
+return x_4;
+}
+}
+LEAN_EXPORT lean_object* l_List_forIn_x27___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; 
+lean_inc(x_2);
+x_5 = l_List_forIn_x27_loop___rarg(x_1, x_2, x_4, x_2, x_3, lean_box(0));
+return x_5;
+}
+}
+LEAN_EXPORT lean_object* l_List_forIn_x27(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = lean_alloc_closure((void*)(l_List_forIn_x27___rarg), 4, 0);
+return x_4;
+}
+}
+LEAN_EXPORT lean_object* l_List_instForIn_x27ListInstMembershipList___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; 
+lean_inc(x_2);
+x_5 = l_List_forIn_x27_loop___rarg(x_1, x_2, x_4, x_2, x_3, lean_box(0));
+return x_5;
+}
+}
+LEAN_EXPORT lean_object* l_List_instForIn_x27ListInstMembershipList(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = lean_alloc_closure((void*)(l_List_instForIn_x27ListInstMembershipList___rarg), 4, 0);
+return x_4;
+}
+}
 LEAN_EXPORT lean_object* l_List_instForMList___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {

stage0/stdlib/Init/NotationExtra.c

@@ -614,6 +614,7 @@ static lean_object* l___aux__Init__NotationExtra______macroRules__command__Class
 LEAN_EXPORT lean_object* l___aux__Init__NotationExtra______macroRules__term___xd7____1__1(lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_expandExplicitBindersAux_loop___closed__8;
 static lean_object* l_term_u03a3_x27___x2c_____closed__5;
+static lean_object* l_Lean___aux__Init__NotationExtra______macroRules__Lean__doElemRepeat____1___closed__18;
 static lean_object* l_Lean_binderIdent___closed__2;
 lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
 static lean_object* l_Lean_binderIdent___closed__1;
@@ -14816,6 +14817,16 @@ return x_3;
 static lean_object* _init_l_Lean___aux__Init__NotationExtra______macroRules__Lean__doElemRepeat____1___closed__17() {
 _start:
 {
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_unexpandExists___closed__5;
+x_2 = l_Lean___aux__Init__NotationExtra______macroRules__Lean__termMacro_x2etrace_x5b_____x5d____1___closed__28;
+x_3 = lean_array_push(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l_Lean___aux__Init__NotationExtra______macroRules__Lean__doElemRepeat____1___closed__18() {
+_start:
+{
 lean_object* x_1; 
 x_1 = lean_mk_string("do");
 return x_1;
@@ -14890,7 +14901,7 @@ lean_ctor_set(x_30, 0, x_12);
 lean_ctor_set(x_30, 1, x_28);
 lean_ctor_set(x_30, 2, x_27);
 lean_ctor_set(x_30, 3, x_29);
-x_31 = l_Lean___aux__Init__NotationExtra______macroRules__Lean__termMacro_x2etrace_x5b_____x5d____1___closed__30;
+x_31 = l_Lean___aux__Init__NotationExtra______macroRules__Lean__doElemRepeat____1___closed__17;
 x_32 = lean_array_push(x_31, x_23);
 x_33 = lean_array_push(x_32, x_25);
 x_34 = lean_array_push(x_33, x_30);
@@ -14905,7 +14916,7 @@ x_39 = lean_alloc_ctor(1, 3, 0);
 lean_ctor_set(x_39, 0, x_21);
 lean_ctor_set(x_39, 1, x_38);
 lean_ctor_set(x_39, 2, x_37);
-x_40 = l_Lean___aux__Init__NotationExtra______macroRules__Lean__doElemRepeat____1___closed__17;
+x_40 = l_Lean___aux__Init__NotationExtra______macroRules__Lean__doElemRepeat____1___closed__18;
 x_41 = lean_alloc_ctor(2, 2, 0);
 lean_ctor_set(x_41, 0, x_12);
 lean_ctor_set(x_41, 1, x_40);
@@ -14968,7 +14979,7 @@ lean_ctor_set(x_68, 0, x_49);
 lean_ctor_set(x_68, 1, x_66);
 lean_ctor_set(x_68, 2, x_65);
 lean_ctor_set(x_68, 3, x_67);
-x_69 = l_Lean___aux__Init__NotationExtra______macroRules__Lean__termMacro_x2etrace_x5b_____x5d____1___closed__30;
+x_69 = l_Lean___aux__Init__NotationExtra______macroRules__Lean__doElemRepeat____1___closed__17;
 x_70 = lean_array_push(x_69, x_61);
 x_71 = lean_array_push(x_70, x_63);
 x_72 = lean_array_push(x_71, x_68);
@@ -14983,7 +14994,7 @@ x_77 = lean_alloc_ctor(1, 3, 0);
 lean_ctor_set(x_77, 0, x_59);
 lean_ctor_set(x_77, 1, x_76);
 lean_ctor_set(x_77, 2, x_75);
-x_78 = l_Lean___aux__Init__NotationExtra______macroRules__Lean__doElemRepeat____1___closed__17;
+x_78 = l_Lean___aux__Init__NotationExtra______macroRules__Lean__doElemRepeat____1___closed__18;
 x_79 = lean_alloc_ctor(2, 2, 0);
 lean_ctor_set(x_79, 0, x_49);
 lean_ctor_set(x_79, 1, x_78);
@@ -15671,7 +15682,7 @@ lean_inc(x_14);
 x_16 = lean_alloc_ctor(2, 2, 0);
 lean_ctor_set(x_16, 0, x_14);
 lean_ctor_set(x_16, 1, x_15);
-x_17 = l_Lean___aux__Init__NotationExtra______macroRules__Lean__doElemRepeat____1___closed__17;
+x_17 = l_Lean___aux__Init__NotationExtra______macroRules__Lean__doElemRepeat____1___closed__18;
 lean_inc(x_14);
 x_18 = lean_alloc_ctor(2, 2, 0);
 lean_ctor_set(x_18, 0, x_14);
@@ -15801,7 +15812,7 @@ lean_inc(x_78);
 x_81 = lean_alloc_ctor(2, 2, 0);
 lean_ctor_set(x_81, 0, x_78);
 lean_ctor_set(x_81, 1, x_80);
-x_82 = l_Lean___aux__Init__NotationExtra______macroRules__Lean__doElemRepeat____1___closed__17;
+x_82 = l_Lean___aux__Init__NotationExtra______macroRules__Lean__doElemRepeat____1___closed__18;
 lean_inc(x_78);
 x_83 = lean_alloc_ctor(2, 2, 0);
 lean_ctor_set(x_83, 0, x_78);
@@ -16982,6 +16993,8 @@ l_Lean___aux__Init__NotationExtra______macroRules__Lean__doElemRepeat____1___clo
 lean_mark_persistent(l_Lean___aux__Init__NotationExtra______macroRules__Lean__doElemRepeat____1___closed__16);
 l_Lean___aux__Init__NotationExtra______macroRules__Lean__doElemRepeat____1___closed__17 = _init_l_Lean___aux__Init__NotationExtra______macroRules__Lean__doElemRepeat____1___closed__17();
 lean_mark_persistent(l_Lean___aux__Init__NotationExtra______macroRules__Lean__doElemRepeat____1___closed__17);
+l_Lean___aux__Init__NotationExtra______macroRules__Lean__doElemRepeat____1___closed__18 = _init_l_Lean___aux__Init__NotationExtra______macroRules__Lean__doElemRepeat____1___closed__18();
+lean_mark_persistent(l_Lean___aux__Init__NotationExtra______macroRules__Lean__doElemRepeat____1___closed__18);
 l_Lean_doElemWhile__Do_____closed__1 = _init_l_Lean_doElemWhile__Do_____closed__1();
 lean_mark_persistent(l_Lean_doElemWhile__Do_____closed__1);
 l_Lean_doElemWhile__Do_____closed__2 = _init_l_Lean_doElemWhile__Do_____closed__2();