bump to nightly-2023-04-05-20

mathlib commit leanprover-community/mathlib@1a4df69

Mathbin/Data/String/Basic.lean

@@ -20,6 +20,7 @@ Supplementary theorems about the `string` type.
 
 namespace String
 
+#print String.ltb /-
 /-- `<` on string iterators. This coincides with `<` on strings as lists. -/
 def ltb : Iterator → Iterator → Bool
   | s₁, s₂ => by
@@ -34,14 +35,25 @@ def ltb : Iterator → Iterator → Bool
       else s₁.curr < s₂.curr termination_by'
   ⟨_, measure_wf fun s => s.1.2.length⟩
 #align string.ltb String.ltb
+-/
 
-instance hasLt' : LT String :=
+#print String.LT' /-
+instance LT' : LT String :=
   ⟨fun s₁ s₂ => ltb s₁.mkIterator s₂.mkIterator⟩
-#align string.has_lt' String.hasLt'
+#align string.has_lt' String.LT'
+-/
 
-instance decidableLt : @DecidableRel String (· < ·) := by infer_instance
-#align string.decidable_lt String.decidableLt
+#print String.decidableLT /-
+instance decidableLT : @DecidableRel String (· < ·) := by infer_instance
+#align string.decidable_lt String.decidableLT
+-/
 
+/- warning: string.lt_iff_to_list_lt -> String.lt_iff_toList_lt is a dubious translation:
+lean 3 declaration is
+  forall {s₁ : String} {s₂ : String}, Iff (LT.lt.{0} String String.LT' s₁ s₂) (LT.lt.{0} (List.{0} Char) (List.LT'.{0} Char Char.hasLt) (String.toList s₁) (String.toList s₂))
+but is expected to have type
+  forall {s₁ : String} {s₂ : String}, Iff (LT.lt.{0} String String.LT' s₁ s₂) (LT.lt.{0} (List.{0} Char) (List.LT'.{0} Char Char.instLTChar) (String.toList s₁) (String.toList s₂))
+Case conversion may be inaccurate. Consider using '#align string.lt_iff_to_list_lt String.lt_iff_toList_ltₓ'. -/
 -- short-circuit type class inference
 @[simp]
 theorem lt_iff_toList_lt : ∀ {s₁ s₂ : String}, s₁ < s₂ ↔ s₁.toList < s₂.toList
@@ -65,52 +77,98 @@ theorem lt_iff_toList_lt : ∀ {s₁ s₂ : String}, s₁ < s₂ ↔ s₁.toList
         assumption
 #align string.lt_iff_to_list_lt String.lt_iff_toList_lt
 
-instance hasLe : LE String :=
+#print String.LE /-
+instance LE : LE String :=
   ⟨fun s₁ s₂ => ¬s₂ < s₁⟩
-#align string.has_le String.hasLe
+#align string.has_le String.LE
+-/
 
-instance decidableLe : @DecidableRel String (· ≤ ·) := by infer_instance
-#align string.decidable_le String.decidableLe
+#print String.decidableLE /-
+instance decidableLE : @DecidableRel String (· ≤ ·) := by infer_instance
+#align string.decidable_le String.decidableLE
+-/
 
+/- warning: string.le_iff_to_list_le -> String.le_iff_toList_le is a dubious translation:
+lean 3 declaration is
+  forall {s₁ : String} {s₂ : String}, Iff (LE.le.{0} String String.LE s₁ s₂) (LE.le.{0} (List.{0} Char) (List.LE'.{0} Char Char.linearOrder) (String.toList s₁) (String.toList s₂))
+but is expected to have type
+  forall {s₁ : String} {s₂ : String}, Iff (LE.le.{0} String String.LE s₁ s₂) (LE.le.{0} (List.{0} Char) (List.LE'.{0} Char instLinearOrderChar) (String.toList s₁) (String.toList s₂))
+Case conversion may be inaccurate. Consider using '#align string.le_iff_to_list_le String.le_iff_toList_leₓ'. -/
 -- short-circuit type class inference
 @[simp]
 theorem le_iff_toList_le {s₁ s₂ : String} : s₁ ≤ s₂ ↔ s₁.toList ≤ s₂.toList :=
   (not_congr lt_iff_toList_lt).trans not_lt
 #align string.le_iff_to_list_le String.le_iff_toList_le
 
+#print String.toList_inj /-
 theorem toList_inj : ∀ {s₁ s₂}, toList s₁ = toList s₂ ↔ s₁ = s₂
   | ⟨s₁⟩, ⟨s₂⟩ => ⟨congr_arg _, congr_arg _⟩
 #align string.to_list_inj String.toList_inj
+-/
 
+/- warning: string.nil_as_string_eq_empty -> String.nil_asString_eq_empty is a dubious translation:
+lean 3 declaration is
+  Eq.{1} String (List.asString (List.nil.{0} Char)) String.empty
+but is expected to have type
+  Eq.{1} String (List.asString (List.nil.{0} Char)) ""
+Case conversion may be inaccurate. Consider using '#align string.nil_as_string_eq_empty String.nil_asString_eq_emptyₓ'. -/
 theorem nil_asString_eq_empty : [].asString = "" :=
   rfl
 #align string.nil_as_string_eq_empty String.nil_asString_eq_empty
 
+/- warning: string.to_list_empty -> String.toList_empty is a dubious translation:
+lean 3 declaration is
+  Eq.{1} (List.{0} Char) (String.toList String.empty) (List.nil.{0} Char)
+but is expected to have type
+  Eq.{1} (List.{0} Char) (String.toList "") (List.nil.{0} Char)
+Case conversion may be inaccurate. Consider using '#align string.to_list_empty String.toList_emptyₓ'. -/
 @[simp]
 theorem toList_empty : "".toList = [] :=
   rfl
 #align string.to_list_empty String.toList_empty
 
+#print String.asString_inv_toList /-
 theorem asString_inv_toList (s : String) : s.toList.asString = s :=
   by
   cases s
   rfl
 #align string.as_string_inv_to_list String.asString_inv_toList
+-/
 
+#print String.toList_singleton /-
 @[simp]
 theorem toList_singleton (c : Char) : (String.singleton c).toList = [c] :=
   rfl
 #align string.to_list_singleton String.toList_singleton
+-/
 
+/- warning: string.to_list_nonempty -> String.toList_nonempty is a dubious translation:
+lean 3 declaration is
+  forall {s : String}, (Ne.{1} String s String.empty) -> (Eq.{1} (List.{0} Char) (String.toList s) (List.cons.{0} Char (String.head s) (String.toList (String.popn s (OfNat.ofNat.{0} Nat 1 (OfNat.mk.{0} Nat 1 (One.one.{0} Nat Nat.hasOne)))))))
+but is expected to have type
+  forall {s : String}, (Ne.{1} String s "") -> (Eq.{1} (List.{0} Char) (String.toList s) (List.cons.{0} Char (String.head s) (String.toList (String.popn s (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))))))
+Case conversion may be inaccurate. Consider using '#align string.to_list_nonempty String.toList_nonemptyₓ'. -/
 theorem toList_nonempty : ∀ {s : String}, s ≠ String.empty → s.toList = s.headI :: (s.popn 1).toList
   | ⟨s⟩, h => by cases s <;> [cases h rfl, rfl]
 #align string.to_list_nonempty String.toList_nonempty
 
+/- warning: string.head_empty -> String.head_empty is a dubious translation:
+lean 3 declaration is
+  Eq.{1} Char (String.head String.empty) (Inhabited.default.{1} Char Char.inhabited)
+but is expected to have type
+  Eq.{1} Char (List.head!.{0} Char Char.instInhabitedChar (String.data "")) (Inhabited.default.{1} Char Char.instInhabitedChar)
+Case conversion may be inaccurate. Consider using '#align string.head_empty String.head_emptyₓ'. -/
 @[simp]
 theorem head_empty : "".headI = default :=
   rfl
 #align string.head_empty String.head_empty
 
+/- warning: string.popn_empty -> String.popn_empty is a dubious translation:
+lean 3 declaration is
+  forall {n : Nat}, Eq.{1} String (String.popn String.empty n) String.empty
+but is expected to have type
+  forall {n : Nat}, Eq.{1} String (String.popn "" n) ""
+Case conversion may be inaccurate. Consider using '#align string.popn_empty String.popn_emptyₓ'. -/
 @[simp]
 theorem popn_empty {n : ℕ} : "".popn n = "" :=
   by
@@ -127,7 +185,7 @@ instance : LinearOrder String where
   lt := (· < ·)
   le := (· ≤ ·)
   decidableLt := by infer_instance
-  decidableLe := String.decidableLe
+  decidableLe := String.decidableLE
   DecidableEq := by infer_instance
   le_refl a := le_iff_toList_le.2 le_rfl
   le_trans a b c := by
@@ -145,29 +203,39 @@ end String
 
 open String
 
+#print List.toList_inv_asString /-
 theorem List.toList_inv_asString (l : List Char) : l.asString.toList = l :=
   by
   cases hl : l.as_string
   exact StringImp.mk.inj hl.symm
 #align list.to_list_inv_as_string List.toList_inv_asString
+-/
 
+#print List.length_asString /-
 @[simp]
 theorem List.length_asString (l : List Char) : l.asString.length = l.length :=
   rfl
 #align list.length_as_string List.length_asString
+-/
 
+#print List.asString_inj /-
 @[simp]
 theorem List.asString_inj {l l' : List Char} : l.asString = l'.asString ↔ l = l' :=
   ⟨fun h => by rw [← List.toList_inv_asString l, ← List.toList_inv_asString l', to_list_inj, h],
     fun h => h ▸ rfl⟩
 #align list.as_string_inj List.asString_inj
+-/
 
+#print String.length_toList /-
 @[simp]
 theorem String.length_toList (s : String) : s.toList.length = s.length := by
   rw [← String.asString_inv_toList s, List.toList_inv_asString, List.length_asString]
 #align string.length_to_list String.length_toList
+-/
 
+#print List.asString_eq /-
 theorem List.asString_eq {l : List Char} {s : String} : l.asString = s ↔ l = s.toList := by
   rw [← as_string_inv_to_list s, List.asString_inj, as_string_inv_to_list s]
 #align list.as_string_eq List.asString_eq
+-/
 

Mathbin/Data/String/Defs.lean

@@ -70,10 +70,12 @@ def getRest (s t : String) : Option String :=
   List.asString <$> s.toList.getRest t.toList
 #align string.get_rest String.getRest
 
+#print String.popn /-
 /-- Removes the first `n` elements from the string `s` -/
 def popn (s : String) (n : Nat) : String :=
   (s.mkIterator.nextn n).nextToString
 #align string.popn String.popn
+-/
 
 #print String.isNat /-
 /-- `is_nat s` is true iff `s` is a nonempty sequence of digits. -/
@@ -82,10 +84,12 @@ def isNat (s : String) : Bool :=
 #align string.is_nat String.isNat
 -/
 
+#print String.head /-
 /-- Produce the head character from the string `s`, if `s` is not empty, otherwise 'A'. -/
 def head (s : String) : Char :=
   s.mkIterator.curr
 #align string.head String.head
+-/
 
 end String
 

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "4e45389235cc80af62200e1cfe04be66e5349dbd",
+    "rev": "9d12b4b0d4d8c339cd23f64abf2d299511d3988c",
     "name": "lean3port",
-    "inputRev?": "4e45389235cc80af62200e1cfe04be66e5349dbd"}},
+    "inputRev?": "9d12b4b0d4d8c339cd23f64abf2d299511d3988c"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "41bcd06badc26638f4162b20ea549b0a506705b8",
+    "rev": "0fdb96c1a537978167d6a528433976959540b444",
     "name": "mathlib",
-    "inputRev?": "41bcd06badc26638f4162b20ea549b0a506705b8"}},
+    "inputRev?": "0fdb96c1a537978167d6a528433976959540b444"}},
   {"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-04-05-18"
+def tag : String := "nightly-2023-04-05-20"
 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"@"4e45389235cc80af62200e1cfe04be66e5349dbd"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"9d12b4b0d4d8c339cd23f64abf2d299511d3988c"
 
 @[default_target]
 lean_lib Mathbin where