chore(*): update to lean 3.42.0c (#12818)

leanpkg.toml

@@ -1,7 +1,7 @@
 [package]
 name = "mathlib"
 version = "0.1"
-lean_version = "leanprover-community/lean:3.41.0"
+lean_version = "leanprover-community/lean:3.42.0"
 path = "src"
 
 [dependencies]

src/tactic/interactive.lean

@@ -204,6 +204,7 @@ private meta def generalize_arg_p : parser (pexpr × name) :=
 with_desc "expr = id" $ parser.pexpr 0 >>= generalize_arg_p_aux
 
 @[nolint def_lemma]
+noncomputable
 lemma {u} generalize_a_aux {α : Sort u}
   (h : ∀ x : Sort u, (α → x) → x) : α := h α id
 

test/induction.lean

@@ -787,7 +787,7 @@ inductive lte : nat → nat → Type
 | zero (n : nat) : lte 0 n
 | succ {n m : nat} : lte n m → lte (1 + n) (1 + m)
 
-lemma lt_lte {n m} : lt n m → lte n m :=
+def lt_lte {n m} : lt n m → lte n m :=
 begin
   intro lt_n_m,
   induction' lt_n_m,

test/lint.lean

@@ -5,7 +5,7 @@ open tactic
 
 def foo1 (n m : ℕ) : ℕ := n + 1
 def foo2 (n m : ℕ) : m = m := by refl
-lemma foo3 (n m : ℕ) : ℕ := n - m
+noncomputable lemma foo3 (n m : ℕ) : ℕ := n - m
 lemma foo.foo (n m : ℕ) : n ≥ n := le_refl n
 instance bar.bar : has_add ℕ := by apply_instance  -- we don't check the name of instances
 lemma foo.bar (ε > 0) : ε = ε := rfl -- >/≥ is allowed in binders (and in fact, in all hypotheses)

test/lint_to_additive_doc.lean

@@ -2,19 +2,19 @@ import algebra.group.to_additive
 
 /-- Docstring -/
 @[to_additive add_foo]
-lemma foo (α : Type*) [has_one α] : α := 1
+def foo (α : Type*) [has_one α] : α := 1
 
 @[to_additive add_bar "docstring"]
-lemma bar (α : Type*) [has_one α] : α := 1
+def bar (α : Type*) [has_one α] : α := 1
 
 /-- Docstring -/
 @[to_additive add_baz "docstring"]
-lemma baz (α : Type*) [has_one α] : α := 1
+def baz (α : Type*) [has_one α] : α := 1
 
 @[to_additive add_quuz]
-lemma quux (α : Type*) [has_one α] : α := 1
+def quux (α : Type*) [has_one α] : α := 1
 
-lemma no_to_additive (α : Type*) [has_one α] : α := 1
+def no_to_additive (α : Type*) [has_one α] : α := 1
 
 open tactic
 run_cmd do

test/local_cache.lean

@@ -90,6 +90,7 @@ def my_definition' : dummy :=
      exact 1
    end, ⟩
 
+noncomputable
 lemma my_lemma' : dummy :=
  ⟨ begin
      my_tactic,
@@ -308,6 +309,7 @@ def my_definition' : dummy :=
      exact 1
    end, ⟩
 
+noncomputable
 lemma my_lemma' : dummy :=
  ⟨ begin
      my_tactic,