feat(*): bump to nightly-2021-10-02 (leanprover#54)

ChrisHughes24 · Oct 2, 2021 · 210fc85 · 210fc85
1 parent 4e2e759
commit 210fc85
Show file tree

Hide file tree

Showing 5 changed files with 4 additions and 5 deletions.
diff --git a/Mathlib/Data/Nat/Basic.lean b/Mathlib/Data/Nat/Basic.lean
@@ -99,6 +99,6 @@ def Up (ub a i : ℕ) := i < a ∧ i < ub
 lemma Up.next {ub i} (h : i < ub) : Up ub (i+1) i := ⟨Nat.lt_succ_self _, h⟩
 
 lemma Up.WF (ub) : WellFounded (Up ub) :=
-  Subrelation.wf (h₂ := measure (ub - .)) @fun a i ⟨ia, iu⟩ => Nat.sub_lt_sub_left iu ia
+  Subrelation.wf (h₂ := (measure (ub - .)).wf) @fun a i ⟨ia, iu⟩ => Nat.sub_lt_sub_left iu ia
 
 end Nat
diff --git a/Mathlib/Data/Nat/Gcd.lean b/Mathlib/Data/Nat/Gcd.lean
@@ -48,7 +48,7 @@ theorem gcd.induction
   (H0 : ∀n, P 0 n)
   (H1 : ∀ m n, 0 < m → P (n % m) m → P m n) :
   P m n :=
-  @WellFounded.induction _ _ lt_wf (λ m => ∀ n, P m n) m
+  @WellFounded.induction _ _ lt_wfRel.wf (λ m => ∀ n, P m n) m
     (λ k IH =>
       match k with
       | 0 => H0

diff --git a/Mathlib/Init/Data/Nat/Lemmas.lean b/Mathlib/Init/Data/Nat/Lemmas.lean
@@ -236,7 +236,7 @@ by rw [sub_eq_sub_min, Nat.sub_add_cancel (min_le_left n m)]
 
 protected def strong_rec_on {p : ℕ → Sort u}
   (n : ℕ) (H : ∀ n, (∀ m, m < n → p m) → p n) : p n :=
-Nat.lt_wf.fix' H n
+Nat.lt_wfRel.wf.fix' H n
 
 protected lemma strong_induction_on {p : Nat → Prop} (n : Nat) (h : ∀ n, (∀ m, m < n → p m) → p n) : p n :=
 Nat.strong_rec_on n h

diff --git a/Mathlib/Init/Logic.lean b/Mathlib/Init/Logic.lean
@@ -590,4 +590,3 @@ set_option codegen false in
 def fix' (hwf : WellFounded r) (F : ∀ x, (∀ y, r y x → C y) → C x) (x : α) : C x := hwf.fix F x
 
 end WellFounded
-
diff --git a/leanpkg.toml b/leanpkg.toml
@@ -1,4 +1,4 @@
 [package]
 name = "mathlib4"
 version = "0.1"
-lean_version = "leanprover/lean4:nightly-2021-09-24"
+lean_version = "leanprover/lean4:nightly-2021-10-02"
Original file line number	Diff line number	Diff line change
Expand Up		@@ -590,4 +590,3 @@ set_option codegen false in
		def fix' (hwf : WellFounded r) (F : ∀ x, (∀ y, r y x → C y) → C x) (x : α) : C x := hwf.fix F x

		end WellFounded