bump to nightly-2023-05-17-18

mathlib commit leanprover-community/mathlib@f8c79b0

Mathbin/Data/Seq/Computation.lean

@@ -1148,7 +1148,7 @@ instance : Alternative Computation :=
 lean 3 declaration is
   forall {α : Type.{u1}} (a : α) (c₂ : Computation.{u1} α), Eq.{succ u1} (Computation.{u1} α) (HasOrelse.orelse.{u1, u1} Computation.{u1} (Alternative.toHasOrelse.{u1, u1} Computation.{u1} Computation.alternative.{u1}) α (Computation.pure.{u1} α a) c₂) (Computation.pure.{u1} α a)
 but is expected to have type
-  forall {α : Type.{u1}} (a : α) (c₂ : Computation.{u1} α), Eq.{succ u1} (Computation.{u1} α) (HOrElse.hOrElse.{u1, u1, u1} (Computation.{u1} α) (Computation.{u1} α) (Computation.{u1} α) (instHOrElse.{u1} (Computation.{u1} α) (instOrElse.{u1, u1} Computation.{u1} α Computation.instAlternativeComputation.{u1})) (Computation.pure.{u1} α a) (fun (x._@.Mathlib.Data.Seq.Computation._hyg.10376 : Unit) => c₂)) (Computation.pure.{u1} α a)
+  forall {α : Type.{u1}} (a : α) (c₂ : Computation.{u1} α), Eq.{succ u1} (Computation.{u1} α) (HOrElse.hOrElse.{u1, u1, u1} (Computation.{u1} α) (Computation.{u1} α) (Computation.{u1} α) (instHOrElse.{u1} (Computation.{u1} α) (instOrElse.{u1, u1} Computation.{u1} α Computation.instAlternativeComputation.{u1})) (Computation.pure.{u1} α a) (fun (x._@.Mathlib.Data.Seq.Computation._hyg.10321 : Unit) => c₂)) (Computation.pure.{u1} α a)
 Case conversion may be inaccurate. Consider using '#align computation.ret_orelse Computation.ret_orElseₓ'. -/
 @[simp]
 theorem ret_orElse (a : α) (c₂ : Computation α) : (pure a <|> c₂) = pure a :=
@@ -1159,7 +1159,7 @@ theorem ret_orElse (a : α) (c₂ : Computation α) : (pure a <|> c₂) = pure a
 lean 3 declaration is
   forall {α : Type.{u1}} (c₁ : Computation.{u1} α) (a : α), Eq.{succ u1} (Computation.{u1} α) (HasOrelse.orelse.{u1, u1} Computation.{u1} (Alternative.toHasOrelse.{u1, u1} Computation.{u1} Computation.alternative.{u1}) α (Computation.think.{u1} α c₁) (Computation.pure.{u1} α a)) (Computation.pure.{u1} α a)
 but is expected to have type
-  forall {α : Type.{u1}} (c₁ : Computation.{u1} α) (a : α), Eq.{succ u1} (Computation.{u1} α) (HOrElse.hOrElse.{u1, u1, u1} (Computation.{u1} α) (Computation.{u1} α) (Computation.{u1} α) (instHOrElse.{u1} (Computation.{u1} α) (instOrElse.{u1, u1} Computation.{u1} α Computation.instAlternativeComputation.{u1})) (Computation.think.{u1} α c₁) (fun (x._@.Mathlib.Data.Seq.Computation._hyg.10404 : Unit) => Computation.pure.{u1} α a)) (Computation.pure.{u1} α a)
+  forall {α : Type.{u1}} (c₁ : Computation.{u1} α) (a : α), Eq.{succ u1} (Computation.{u1} α) (HOrElse.hOrElse.{u1, u1, u1} (Computation.{u1} α) (Computation.{u1} α) (Computation.{u1} α) (instHOrElse.{u1} (Computation.{u1} α) (instOrElse.{u1, u1} Computation.{u1} α Computation.instAlternativeComputation.{u1})) (Computation.think.{u1} α c₁) (fun (x._@.Mathlib.Data.Seq.Computation._hyg.10349 : Unit) => Computation.pure.{u1} α a)) (Computation.pure.{u1} α a)
 Case conversion may be inaccurate. Consider using '#align computation.orelse_ret Computation.orelse_pureₓ'. -/
 @[simp]
 theorem orelse_pure (c₁ : Computation α) (a : α) : (think c₁ <|> pure a) = pure a :=
@@ -1170,7 +1170,7 @@ theorem orelse_pure (c₁ : Computation α) (a : α) : (think c₁ <|> pure a) =
 lean 3 declaration is
   forall {α : Type.{u1}} (c₁ : Computation.{u1} α) (c₂ : Computation.{u1} α), Eq.{succ u1} (Computation.{u1} α) (HasOrelse.orelse.{u1, u1} Computation.{u1} (Alternative.toHasOrelse.{u1, u1} Computation.{u1} Computation.alternative.{u1}) α (Computation.think.{u1} α c₁) (Computation.think.{u1} α c₂)) (Computation.think.{u1} α (HasOrelse.orelse.{u1, u1} Computation.{u1} (Alternative.toHasOrelse.{u1, u1} Computation.{u1} Computation.alternative.{u1}) α c₁ c₂))
 but is expected to have type
-  forall {α : Type.{u1}} (c₁ : Computation.{u1} α) (c₂ : Computation.{u1} α), Eq.{succ u1} (Computation.{u1} α) (HOrElse.hOrElse.{u1, u1, u1} (Computation.{u1} α) (Computation.{u1} α) (Computation.{u1} α) (instHOrElse.{u1} (Computation.{u1} α) (instOrElse.{u1, u1} Computation.{u1} α Computation.instAlternativeComputation.{u1})) (Computation.think.{u1} α c₁) (fun (x._@.Mathlib.Data.Seq.Computation._hyg.10440 : Unit) => Computation.think.{u1} α c₂)) (Computation.think.{u1} α (HOrElse.hOrElse.{u1, u1, u1} (Computation.{u1} α) (Computation.{u1} α) (Computation.{u1} α) (instHOrElse.{u1} (Computation.{u1} α) (instOrElse.{u1, u1} Computation.{u1} α Computation.instAlternativeComputation.{u1})) c₁ (fun (x._@.Mathlib.Data.Seq.Computation._hyg.10439 : Unit) => c₂)))
+  forall {α : Type.{u1}} (c₁ : Computation.{u1} α) (c₂ : Computation.{u1} α), Eq.{succ u1} (Computation.{u1} α) (HOrElse.hOrElse.{u1, u1, u1} (Computation.{u1} α) (Computation.{u1} α) (Computation.{u1} α) (instHOrElse.{u1} (Computation.{u1} α) (instOrElse.{u1, u1} Computation.{u1} α Computation.instAlternativeComputation.{u1})) (Computation.think.{u1} α c₁) (fun (x._@.Mathlib.Data.Seq.Computation._hyg.10385 : Unit) => Computation.think.{u1} α c₂)) (Computation.think.{u1} α (HOrElse.hOrElse.{u1, u1, u1} (Computation.{u1} α) (Computation.{u1} α) (Computation.{u1} α) (instHOrElse.{u1} (Computation.{u1} α) (instOrElse.{u1, u1} Computation.{u1} α Computation.instAlternativeComputation.{u1})) c₁ (fun (x._@.Mathlib.Data.Seq.Computation._hyg.10384 : Unit) => c₂)))
 Case conversion may be inaccurate. Consider using '#align computation.orelse_think Computation.orelse_thinkₓ'. -/
 @[simp]
 theorem orelse_think (c₁ c₂ : Computation α) : (think c₁ <|> think c₂) = think (c₁ <|> c₂) :=
@@ -1181,7 +1181,7 @@ theorem orelse_think (c₁ c₂ : Computation α) : (think c₁ <|> think c₂)
 lean 3 declaration is
   forall {α : Type.{u1}} (c : Computation.{u1} α), Eq.{succ u1} (Computation.{u1} α) (HasOrelse.orelse.{u1, u1} Computation.{u1} (Alternative.toHasOrelse.{u1, u1} Computation.{u1} Computation.alternative.{u1}) α (Computation.empty.{u1} α) c) c
 but is expected to have type
-  forall {α : Type.{u1}} (c : Computation.{u1} α), Eq.{succ u1} (Computation.{u1} α) (HOrElse.hOrElse.{u1, u1, u1} (Computation.{u1} α) (Computation.{u1} α) (Computation.{u1} α) (instHOrElse.{u1} (Computation.{u1} α) (instOrElse.{u1, u1} Computation.{u1} α Computation.instAlternativeComputation.{u1})) (Computation.empty.{u1} α) (fun (x._@.Mathlib.Data.Seq.Computation._hyg.10464 : Unit) => c)) c
+  forall {α : Type.{u1}} (c : Computation.{u1} α), Eq.{succ u1} (Computation.{u1} α) (HOrElse.hOrElse.{u1, u1, u1} (Computation.{u1} α) (Computation.{u1} α) (Computation.{u1} α) (instHOrElse.{u1} (Computation.{u1} α) (instOrElse.{u1, u1} Computation.{u1} α Computation.instAlternativeComputation.{u1})) (Computation.empty.{u1} α) (fun (x._@.Mathlib.Data.Seq.Computation._hyg.10409 : Unit) => c)) c
 Case conversion may be inaccurate. Consider using '#align computation.empty_orelse Computation.empty_orelseₓ'. -/
 @[simp]
 theorem empty_orelse (c) : (empty α <|> c) = c :=
@@ -1196,7 +1196,7 @@ theorem empty_orelse (c) : (empty α <|> c) = c :=
 lean 3 declaration is
   forall {α : Type.{u1}} (c : Computation.{u1} α), Eq.{succ u1} (Computation.{u1} α) (HasOrelse.orelse.{u1, u1} Computation.{u1} (Alternative.toHasOrelse.{u1, u1} Computation.{u1} Computation.alternative.{u1}) α c (Computation.empty.{u1} α)) c
 but is expected to have type
-  forall {α : Type.{u1}} (c : Computation.{u1} α), Eq.{succ u1} (Computation.{u1} α) (HOrElse.hOrElse.{u1, u1, u1} (Computation.{u1} α) (Computation.{u1} α) (Computation.{u1} α) (instHOrElse.{u1} (Computation.{u1} α) (instOrElse.{u1, u1} Computation.{u1} α Computation.instAlternativeComputation.{u1})) c (fun (x._@.Mathlib.Data.Seq.Computation._hyg.10662 : Unit) => Computation.empty.{u1} α)) c
+  forall {α : Type.{u1}} (c : Computation.{u1} α), Eq.{succ u1} (Computation.{u1} α) (HOrElse.hOrElse.{u1, u1, u1} (Computation.{u1} α) (Computation.{u1} α) (Computation.{u1} α) (instHOrElse.{u1} (Computation.{u1} α) (instOrElse.{u1, u1} Computation.{u1} α Computation.instAlternativeComputation.{u1})) c (fun (x._@.Mathlib.Data.Seq.Computation._hyg.10607 : Unit) => Computation.empty.{u1} α)) c
 Case conversion may be inaccurate. Consider using '#align computation.orelse_empty Computation.orelse_emptyₓ'. -/
 @[simp]
 theorem orelse_empty (c : Computation α) : (c <|> empty α) = c :=

Mathbin/Data/Stream/Init.lean

@@ -843,11 +843,15 @@ theorem mem_cycle {a : α} {l : List α} : ∀ h : l ≠ [], a ∈ l → a ∈ c
 #align stream.mem_cycle Stream'.mem_cycle
 -/
 
-#print Stream'.cycle_singleton /-
+/- warning: stream.cycle_singleton -> Stream'.cycle_singleton is a dubious translation:
+lean 3 declaration is
+  forall {α : Type.{u1}} (a : α) (h : Ne.{succ u1} (List.{u1} α) (List.cons.{u1} α a (List.nil.{u1} α)) (List.nil.{u1} α)), Eq.{succ u1} (Stream'.{u1} α) (Stream'.cycle.{u1} α (List.cons.{u1} α a (List.nil.{u1} α)) h) (Stream'.const.{u1} α a)
+but is expected to have type
+  forall {α : Type.{u1}} (a : α), Eq.{succ u1} (Stream'.{u1} α) (Stream'.cycle.{u1} α (List.cons.{u1} α a (List.nil.{u1} α)) (of_eq_true (Not (Eq.{succ u1} (List.{u1} α) (List.cons.{u1} α a (List.nil.{u1} α)) (List.nil.{u1} α))) (Eq.trans.{1} Prop (Not (Eq.{succ u1} (List.{u1} α) (List.cons.{u1} α a (List.nil.{u1} α)) (List.nil.{u1} α))) (Not False) True (congrArg.{1, 1} Prop Prop (Eq.{succ u1} (List.{u1} α) (List.cons.{u1} α a (List.nil.{u1} α)) (List.nil.{u1} α)) False Not (eq_false' (Eq.{succ u1} (List.{u1} α) (List.cons.{u1} α a (List.nil.{u1} α)) (List.nil.{u1} α)) (fun (h : Eq.{succ u1} (List.{u1} α) (List.cons.{u1} α a (List.nil.{u1} α)) (List.nil.{u1} α)) => List.noConfusion.{0, u1} α False (List.cons.{u1} α a (List.nil.{u1} α)) (List.nil.{u1} α) h))) not_false_eq_true))) (Stream'.const.{u1} α a)
+Case conversion may be inaccurate. Consider using '#align stream.cycle_singleton Stream'.cycle_singletonₓ'. -/
 theorem cycle_singleton (a : α) (h : [a] ≠ []) : cycle [a] h = const a :=
   coinduction rfl fun β fr ch => by rwa [cycle_eq, const_eq]
 #align stream.cycle_singleton Stream'.cycle_singleton
--/
 
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
 #print Stream'.tails_eq /-

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "3442267303478f548dc5969de6c1e995224fc5d7",
+    "rev": "0d4461ee8ea679c86ea590efd1ec9a1233d2ea04",
     "name": "lean3port",
-    "inputRev?": "3442267303478f548dc5969de6c1e995224fc5d7"}},
+    "inputRev?": "0d4461ee8ea679c86ea590efd1ec9a1233d2ea04"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "3d49f210269bb765621cfc17a634f31257ac4cf6",
+    "rev": "48c72e85b485027693a6aadecccc422af108ff76",
     "name": "mathlib",
-    "inputRev?": "3d49f210269bb765621cfc17a634f31257ac4cf6"}},
+    "inputRev?": "48c72e85b485027693a6aadecccc422af108ff76"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

lakefile.lean

@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-05-17-16"
+def tag : String := "nightly-2023-05-17-18"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"3442267303478f548dc5969de6c1e995224fc5d7"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"0d4461ee8ea679c86ea590efd1ec9a1233d2ea04"
 
 @[default_target]
 lean_lib Mathbin where