feat: add Float.toBits and Float.fromBits

This PR adds raw transmutation of floating-point numbers to and from `UInt64`. Floats and UInts share the same endianness across all supported platforms. The IEEE 754 standard precisely specifies the bit layout of floats. Note that `Float.toBits` is distinct from `Float.toUInt64`, which attempts to preserve the numeric value rather than the bitwise value.

.github/workflows/pr-body.yml

@@ -1,6 +1,7 @@
 name: Check PR body for changelog convention
 
 on:
+  merge_group:
   pull_request:
     types: [opened, synchronize, reopened, edited, labeled, converted_to_draft, ready_for_review]
 
@@ -9,6 +10,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Check PR body
+        if: github.event_name == 'pull_request'
         uses: actions/github-script@v7
         with:
           script: |

nix/bootstrap.nix

@@ -170,7 +170,7 @@ lib.warn "The Nix-based build is deprecated" rec {
           ln -sf ${lean-all}/* .
         '';
         buildPhase = ''
-          ctest --output-junit test-results.xml --output-on-failure -E 'leancomptest_(doc_example|foreign)|leanlaketest_reverse-ffi' -j$NIX_BUILD_CORES
+         ctest --output-junit test-results.xml --output-on-failure -E 'leancomptest_(doc_example|foreign)|leanlaketest_reverse-ffi|leanruntest_timeIO' -j$NIX_BUILD_CORES
         '';
         installPhase = ''
           mkdir $out

src/Init/Core.lean

@@ -1922,12 +1922,12 @@ represents an element of `Squash α` the same as `α` itself
 `Squash.lift` will extract a value in any subsingleton `β` from a function on `α`,
 while `Nonempty.rec` can only do the same when `β` is a proposition.
 -/
-def Squash (α : Type u) := Quot (fun (_ _ : α) => True)
+def Squash (α : Sort u) := Quot (fun (_ _ : α) => True)
 
 /-- The canonical quotient map into `Squash α`. -/
-def Squash.mk {α : Type u} (x : α) : Squash α := Quot.mk _ x
+def Squash.mk {α : Sort u} (x : α) : Squash α := Quot.mk _ x
 
-theorem Squash.ind {α : Type u} {motive : Squash α → Prop} (h : ∀ (a : α), motive (Squash.mk a)) : ∀ (q : Squash α), motive q :=
+theorem Squash.ind {α : Sort u} {motive : Squash α → Prop} (h : ∀ (a : α), motive (Squash.mk a)) : ∀ (q : Squash α), motive q :=
   Quot.ind h
 
 /-- If `β` is a subsingleton, then a function `α → β` lifts to `Squash α → β`. -/

src/Init/Data.lean

@@ -42,3 +42,4 @@ import Init.Data.PLift
 import Init.Data.Zero
 import Init.Data.NeZero
 import Init.Data.Function
+import Init.Data.RArray

src/Init/Data/Array.lean

@@ -18,3 +18,4 @@ import Init.Data.Array.Bootstrap
 import Init.Data.Array.GetLit
 import Init.Data.Array.MapIdx
 import Init.Data.Array.Set
+import Init.Data.Array.Monadic

src/Init/Data/Array/Attach.lean

@@ -10,6 +10,16 @@ import Init.Data.List.Attach
 
 namespace Array
 
+/-- `O(n)`. Partial map. If `f : Π a, P a → β` is a partial function defined on
+  `a : α` satisfying `P`, then `pmap f l h` is essentially the same as `map f l`
+  but is defined only when all members of `l` satisfy `P`, using the proof
+  to apply `f`.
+
+We replace this at runtime with a more efficient version via
+-/
+def pmap {P : α → Prop} (f : ∀ a, P a → β) (l : Array α) (H : ∀ a ∈ l, P a) : Array β :=
+  (l.toList.pmap f (fun a m => H a (mem_def.mpr m))).toArray
+
 /--
 Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of
 `Array {x // P x}` is the same as the input `Array α`.
@@ -35,6 +45,10 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
     l.toArray.attach = (l.attachWith (· ∈ l.toArray) (by simp)).toArray := by
   simp [attach]
 
+@[simp] theorem _root_.List.pmap_toArray {l : List α} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ l.toArray, P a} :
+    l.toArray.pmap f H = (l.pmap f (by simpa using H)).toArray := by
+  simp [pmap]
+
 @[simp] theorem toList_attachWith {l : Array α} {P : α → Prop} {H : ∀ x ∈ l, P x} :
    (l.attachWith P H).toList = l.toList.attachWith P (by simpa [mem_toList] using H) := by
   simp [attachWith]
@@ -43,6 +57,29 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
     l.attach.toList = l.toList.attachWith (· ∈ l) (by simp [mem_toList]) := by
   simp [attach]
 
+@[simp] theorem toList_pmap {l : Array α} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ l, P a} :
+    (l.pmap f H).toList = l.toList.pmap f (fun a m => H a (mem_def.mpr m)) := by
+  simp [pmap]
+
+/-- Implementation of `pmap` using the zero-copy version of `attach`. -/
+@[inline] private def pmapImpl {P : α → Prop} (f : ∀ a, P a → β) (l : Array α) (H : ∀ a ∈ l, P a) :
+    Array β := (l.attachWith _ H).map fun ⟨x, h'⟩ => f x h'
+
+@[csimp] private theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
+  funext α β p f L h'
+  cases L
+  simp only [pmap, pmapImpl, List.attachWith_toArray, List.map_toArray, mk.injEq, List.map_attachWith]
+  apply List.pmap_congr_left
+  intro a m h₁ h₂
+  congr
+
+@[simp] theorem _root_.List.attachWith_mem_toArray {l : List α} :
+    l.attachWith (fun x => x ∈ l.toArray) (fun x h => by simpa using h) =
+      l.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
+  simp only [List.attachWith, List.attach, List.map_pmap]
+  apply List.pmap_congr_left
+  simp
+
 /-! ## unattach
 
 `Array.unattach` is the (one-sided) inverse of `Array.attach`. It is a synonym for `Array.map Subtype.val`.
@@ -83,7 +120,7 @@ def unattach {α : Type _} {p : α → Prop} (l : Array { x // p x }) := l.map (
 
 @[simp] theorem unattach_attach {l : Array α} : l.attach.unattach = l := by
   cases l
-  simp
+  simp only [List.attach_toArray, List.unattach_toArray, List.unattach_attachWith]
 
 @[simp] theorem unattach_attachWith {p : α → Prop} {l : Array α}
     {H : ∀ a ∈ l, p a} :

src/Init/Data/Array/Basic.lean

@@ -442,6 +442,8 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
   decreasing_by simp_wf; decreasing_trivial_pre_omega
   map 0 (mkEmpty as.size)
 
+@[deprecated mapM (since := "2024-11-11")] abbrev sequenceMap := @mapM
+
 /-- Variant of `mapIdxM` which receives the index as a `Fin as.size`. -/
 @[inline]
 def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]

src/Init/Data/Array/Bootstrap.lean

@@ -15,26 +15,26 @@ This file contains some theorems about `Array` and `List` needed for `Init.Data.
 
 namespace Array
 
-theorem foldlM_eq_foldlM_toList.aux [Monad m]
+theorem foldlM_toList.aux [Monad m]
     (f : β → α → m β) (arr : Array α) (i j) (H : arr.size ≤ i + j) (b) :
     foldlM.loop f arr arr.size (Nat.le_refl _) i j b = (arr.toList.drop j).foldlM f b := by
   unfold foldlM.loop
   split; split
   · cases Nat.not_le_of_gt ‹_› (Nat.zero_add _ ▸ H)
   · rename_i i; rw [Nat.succ_add] at H
-    simp [foldlM_eq_foldlM_toList.aux f arr i (j+1) H]
+    simp [foldlM_toList.aux f arr i (j+1) H]
     rw (occs := .pos [2]) [← List.getElem_cons_drop_succ_eq_drop ‹_›]
     rfl
   · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
 
-theorem foldlM_eq_foldlM_toList [Monad m]
+@[simp] theorem foldlM_toList [Monad m]
     (f : β → α → m β) (init : β) (arr : Array α) :
-    arr.foldlM f init = arr.toList.foldlM f init := by
-  simp [foldlM, foldlM_eq_foldlM_toList.aux]
+    arr.toList.foldlM f init = arr.foldlM f init := by
+  simp [foldlM, foldlM_toList.aux]
 
-theorem foldl_eq_foldl_toList (f : β → α → β) (init : β) (arr : Array α) :
-    arr.foldl f init = arr.toList.foldl f init :=
-  List.foldl_eq_foldlM .. ▸ foldlM_eq_foldlM_toList ..
+@[simp] theorem foldl_toList (f : β → α → β) (init : β) (arr : Array α) :
+    arr.toList.foldl f init = arr.foldl f init :=
+  List.foldl_eq_foldlM .. ▸ foldlM_toList ..
 
 theorem foldrM_eq_reverse_foldlM_toList.aux [Monad m]
     (f : α → β → m β) (arr : Array α) (init : β) (i h) :
@@ -51,23 +51,23 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] (f : α → β → m β) (init
   match arr, this with | _, .inl rfl => rfl | arr, .inr h => ?_
   simp [foldrM, h, ← foldrM_eq_reverse_foldlM_toList.aux, List.take_length]
 
-theorem foldrM_eq_foldrM_toList [Monad m]
+@[simp] theorem foldrM_toList [Monad m]
     (f : α → β → m β) (init : β) (arr : Array α) :
-    arr.foldrM f init = arr.toList.foldrM f init := by
+    arr.toList.foldrM f init = arr.foldrM f init := by
   rw [foldrM_eq_reverse_foldlM_toList, List.foldlM_reverse]
 
-theorem foldr_eq_foldr_toList (f : α → β → β) (init : β) (arr : Array α) :
-    arr.foldr f init = arr.toList.foldr f init :=
-  List.foldr_eq_foldrM .. ▸ foldrM_eq_foldrM_toList ..
+@[simp] theorem foldr_toList (f : α → β → β) (init : β) (arr : Array α) :
+    arr.toList.foldr f init = arr.foldr f init :=
+  List.foldr_eq_foldrM .. ▸ foldrM_toList ..
 
 @[simp] theorem push_toList (arr : Array α) (a : α) : (arr.push a).toList = arr.toList ++ [a] := by
   simp [push, List.concat_eq_append]
 
 @[simp] theorem toListAppend_eq (arr : Array α) (l) : arr.toListAppend l = arr.toList ++ l := by
-  simp [toListAppend, foldr_eq_foldr_toList]
+  simp [toListAppend, ← foldr_toList]
 
 @[simp] theorem toListImpl_eq (arr : Array α) : arr.toListImpl = arr.toList := by
-  simp [toListImpl, foldr_eq_foldr_toList]
+  simp [toListImpl, ← foldr_toList]
 
 @[simp] theorem pop_toList (arr : Array α) : arr.pop.toList = arr.toList.dropLast := rfl
 
@@ -76,7 +76,7 @@ theorem foldr_eq_foldr_toList (f : α → β → β) (init : β) (arr : Array α
 @[simp] theorem toList_append (arr arr' : Array α) :
     (arr ++ arr').toList = arr.toList ++ arr'.toList := by
   rw [← append_eq_append]; unfold Array.append
-  rw [foldl_eq_foldl_toList]
+  rw [← foldl_toList]
   induction arr'.toList generalizing arr <;> simp [*]
 
 @[simp] theorem toList_empty : (#[] : Array α).toList = [] := rfl
@@ -98,20 +98,44 @@ theorem foldr_eq_foldr_toList (f : α → β → β) (init : β) (arr : Array α
   rw [← appendList_eq_append]; unfold Array.appendList
   induction l generalizing arr <;> simp [*]
 
-@[deprecated foldlM_eq_foldlM_toList (since := "2024-09-09")]
-abbrev foldlM_eq_foldlM_data := @foldlM_eq_foldlM_toList
+@[deprecated "Use the reverse direction of `foldrM_toList`." (since := "2024-11-13")]
+theorem foldrM_eq_foldrM_toList [Monad m]
+    (f : α → β → m β) (init : β) (arr : Array α) :
+    arr.foldrM f init = arr.toList.foldrM f init := by
+  simp
 
-@[deprecated foldl_eq_foldl_toList (since := "2024-09-09")]
-abbrev foldl_eq_foldl_data := @foldl_eq_foldl_toList
+@[deprecated "Use the reverse direction of `foldlM_toList`." (since := "2024-11-13")]
+theorem foldlM_eq_foldlM_toList [Monad m]
+    (f : β → α → m β) (init : β) (arr : Array α) :
+    arr.foldlM f init = arr.toList.foldlM f init:= by
+  simp
+
+@[deprecated "Use the reverse direction of `foldr_toList`." (since := "2024-11-13")]
+theorem foldr_eq_foldr_toList
+    (f : α → β → β) (init : β) (arr : Array α) :
+    arr.foldr f init = arr.toList.foldr f init := by
+  simp
+
+@[deprecated "Use the reverse direction of `foldl_toList`." (since := "2024-11-13")]
+theorem foldl_eq_foldl_toList
+    (f : β → α → β) (init : β) (arr : Array α) :
+    arr.foldl f init = arr.toList.foldl f init:= by
+  simp
+
+@[deprecated foldlM_toList (since := "2024-09-09")]
+abbrev foldlM_eq_foldlM_data := @foldlM_toList
+
+@[deprecated foldl_toList (since := "2024-09-09")]
+abbrev foldl_eq_foldl_data := @foldl_toList
 
 @[deprecated foldrM_eq_reverse_foldlM_toList (since := "2024-09-09")]
 abbrev foldrM_eq_reverse_foldlM_data := @foldrM_eq_reverse_foldlM_toList
 
-@[deprecated foldrM_eq_foldrM_toList (since := "2024-09-09")]
-abbrev foldrM_eq_foldrM_data := @foldrM_eq_foldrM_toList
+@[deprecated foldrM_toList (since := "2024-09-09")]
+abbrev foldrM_eq_foldrM_data := @foldrM_toList
 
-@[deprecated foldr_eq_foldr_toList (since := "2024-09-09")]
-abbrev foldr_eq_foldr_data := @foldr_eq_foldr_toList
+@[deprecated foldr_toList (since := "2024-09-09")]
+abbrev foldr_eq_foldr_data := @foldr_toList
 
 @[deprecated push_toList (since := "2024-09-09")]
 abbrev push_data := @push_toList

src/Init/Data/Array/Lemmas.lean

@@ -151,15 +151,15 @@ theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List
 
 theorem foldlM_toArray [Monad m] (f : β → α → m β) (init : β) (l : List α) :
     l.toArray.foldlM f init = l.foldlM f init := by
-  rw [foldlM_eq_foldlM_toList]
+  rw [foldlM_toList]
 
 theorem foldr_toArray (f : α → β → β) (init : β) (l : List α) :
     l.toArray.foldr f init = l.foldr f init := by
-  rw [foldr_eq_foldr_toList]
+  rw [foldr_toList]
 
 theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
     l.toArray.foldl f init = l.foldl f init := by
-  rw [foldl_eq_foldl_toList]
+  rw [foldl_toList]
 
 /-- Variant of `foldrM_toArray` with a side condition for the `start` argument. -/
 @[simp] theorem foldrM_toArray' [Monad m] (f : α → β → m β) (init : β) (l : List α)
@@ -174,21 +174,21 @@ theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
     (h : stop = l.toArray.size) :
     l.toArray.foldlM f init 0 stop = l.foldlM f init := by
   subst h
-  rw [foldlM_eq_foldlM_toList]
+  rw [foldlM_toList]
 
 /-- Variant of `foldr_toArray` with a side condition for the `start` argument. -/
 @[simp] theorem foldr_toArray' (f : α → β → β) (init : β) (l : List α)
     (h : start = l.toArray.size) :
     l.toArray.foldr f init start 0 = l.foldr f init := by
   subst h
-  rw [foldr_eq_foldr_toList]
+  rw [foldr_toList]
 
 /-- Variant of `foldl_toArray` with a side condition for the `stop` argument. -/
 @[simp] theorem foldl_toArray' (f : β → α → β) (init : β) (l : List α)
     (h : stop = l.toArray.size) :
     l.toArray.foldl f init 0 stop = l.foldl f init := by
   subst h
-  rw [foldl_eq_foldl_toList]
+  rw [foldl_toList]
 
 @[simp] theorem append_toArray (l₁ l₂ : List α) :
     l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
@@ -202,6 +202,9 @@ theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
 @[simp] theorem foldl_push {l : List α} {as : Array α} : l.foldl Array.push as = as ++ l.toArray := by
   induction l generalizing as <;> simp [*]
 
+@[simp] theorem foldr_push {l : List α} {as : Array α} : l.foldr (fun a b => push b a) as = as ++ l.reverse.toArray := by
+  rw [foldr_eq_foldl_reverse, foldl_push]
+
 @[simp] theorem findSomeM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) :
     l.toArray.findSomeM? f = l.findSomeM? f := by
   rw [Array.findSomeM?]
@@ -362,7 +365,8 @@ namespace Array
 
 theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) :
     (arr.push a).foldrM f init = f a init >>= arr.foldrM f := by
-  simp [foldrM_eq_reverse_foldlM_toList, -size_push]
+  simp only [foldrM_eq_reverse_foldlM_toList, push_toList, List.reverse_append, List.reverse_cons,
+    List.reverse_nil, List.nil_append, List.singleton_append, List.foldlM_cons, List.foldlM_reverse]
 
 /--
 Variant of `foldrM_push` with `h : start = arr.size + 1`
@@ -388,11 +392,11 @@ rather than `(arr.push a).size` as the argument.
 @[inline] def toListRev (arr : Array α) : List α := arr.foldl (fun l t => t :: l) []
 
 @[simp] theorem toListRev_eq (arr : Array α) : arr.toListRev = arr.toList.reverse := by
-  rw [toListRev, foldl_eq_foldl_toList, ← List.foldr_reverse, List.foldr_cons_nil]
+  rw [toListRev, ← foldl_toList, ← List.foldr_reverse, List.foldr_cons_nil]
 
 theorem mapM_eq_foldlM [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
     arr.mapM f = arr.foldlM (fun bs a => bs.push <$> f a) #[] := by
-  rw [mapM, aux, foldlM_eq_foldlM_toList]; rfl
+  rw [mapM, aux, ← foldlM_toList]; rfl
 where
   aux (i r) :
       mapM.map f arr i r = (arr.toList.drop i).foldlM (fun bs a => bs.push <$> f a) r := by
@@ -407,7 +411,7 @@ where
 
 @[simp] theorem toList_map (f : α → β) (arr : Array α) : (arr.map f).toList = arr.toList.map f := by
   rw [map, mapM_eq_foldlM]
-  apply congrArg toList (foldl_eq_foldl_toList (fun bs a => push bs (f a)) #[] arr) |>.trans
+  apply congrArg toList (foldl_toList (fun bs a => push bs (f a)) #[] arr).symm |>.trans
   have H (l arr) : List.foldl (fun bs a => push bs (f a)) arr l = ⟨arr.toList ++ l.map f⟩ := by
     induction l generalizing arr <;> simp [*]
   simp [H]
@@ -1023,7 +1027,7 @@ theorem foldr_congr {as bs : Array α} (h₀ : as = bs) {f g : α → β → β}
 
 theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
     arr.mapM f = List.toArray <$> (arr.toList.mapM f) := by
-  rw [mapM_eq_foldlM, foldlM_eq_foldlM_toList, ← List.foldrM_reverse]
+  rw [mapM_eq_foldlM, ← foldlM_toList, ← List.foldrM_reverse]
   conv => rhs; rw [← List.reverse_reverse arr.toList]
   induction arr.toList.reverse with
   | nil => simp
@@ -1148,7 +1152,7 @@ theorem getElem?_modify {as : Array α} {i : Nat} {f : α → α} {j : Nat} :
 @[simp] theorem toList_filter (p : α → Bool) (l : Array α) :
     (l.filter p).toList = l.toList.filter p := by
   dsimp only [filter]
-  rw [foldl_eq_foldl_toList]
+  rw [← foldl_toList]
   generalize l.toList = l
   suffices ∀ a, (List.foldl (fun r a => if p a = true then push r a else r) a l).toList =
       a.toList ++ List.filter p l by
@@ -1179,7 +1183,7 @@ theorem filter_congr {as bs : Array α} (h : as = bs)
 @[simp] theorem toList_filterMap (f : α → Option β) (l : Array α) :
     (l.filterMap f).toList = l.toList.filterMap f := by
   dsimp only [filterMap, filterMapM]
-  rw [foldlM_eq_foldlM_toList]
+  rw [← foldlM_toList]
   generalize l.toList = l
   have this : ∀ a : Array β, (Id.run (List.foldlM (m := Id) ?_ a l)).toList =
     a.toList ++ List.filterMap f l := ?_
@@ -1258,7 +1262,7 @@ theorem getElem?_append {as bs : Array α} {n : Nat} :
 @[simp] theorem toList_flatten {l : Array (Array α)} :
     l.flatten.toList = (l.toList.map toList).flatten := by
   dsimp [flatten]
-  simp only [foldl_eq_foldl_toList]
+  simp only [← foldl_toList]
   generalize l.toList = l
   have : ∀ a : Array α, (List.foldl ?_ a l).toList = a.toList ++ ?_ := ?_
   exact this #[]

src/Init/Data/Array/Monadic.lean

@@ -0,0 +1,159 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.Array.Lemmas
+import Init.Data.Array.Attach
+import Init.Data.List.Monadic
+
+/-!
+# Lemmas about `Array.forIn'` and `Array.forIn`.
+-/
+
+namespace Array
+
+open Nat
+
+/-! ## Monadic operations -/
+
+/-! ### mapM -/
+
+theorem mapM_eq_foldlM_push [Monad m] [LawfulMonad m] (f : α → m β) (l : Array α) :
+    mapM f l = l.foldlM (fun acc a => return (acc.push (← f a))) #[] := by
+  rcases l with ⟨l⟩
+  simp only [List.mapM_toArray, bind_pure_comp, size_toArray, List.foldlM_toArray']
+  rw [List.mapM_eq_reverse_foldlM_cons]
+  simp only [bind_pure_comp, Functor.map_map]
+  suffices ∀ (k), (fun a => a.reverse.toArray) <$> List.foldlM (fun acc a => (fun a => a :: acc) <$> f a) k l =
+      List.foldlM (fun acc a => acc.push <$> f a) k.reverse.toArray l by
+    exact this []
+  intro k
+  induction l generalizing k with
+  | nil => simp
+  | cons a as ih =>
+    simp [ih, List.foldlM_cons]
+
+/-! ### foldlM and foldrM -/
+
+theorem foldlM_map [Monad m] (f : β₁ → β₂) (g : α → β₂ → m α) (l : Array β₁) (init : α) :
+    (l.map f).foldlM g init = l.foldlM (fun x y => g x (f y)) init := by
+  cases l
+  rw [List.map_toArray] -- Why doesn't this fire via `simp`?
+  simp [List.foldlM_map]
+
+theorem foldrM_map [Monad m] [LawfulMonad m] (f : β₁ → β₂) (g : β₂ → α → m α) (l : Array β₁)
+    (init : α) : (l.map f).foldrM g init = l.foldrM (fun x y => g (f x) y) init := by
+  cases l
+  rw [List.map_toArray] -- Why doesn't this fire via `simp`?
+  simp [List.foldrM_map]
+
+theorem foldlM_filterMap [Monad m] [LawfulMonad m] (f : α → Option β) (g : γ → β → m γ) (l : Array α) (init : γ) :
+    (l.filterMap f).foldlM g init =
+      l.foldlM (fun x y => match f y with | some b => g x b | none => pure x) init := by
+  cases l
+  rw [List.filterMap_toArray] -- Why doesn't this fire via `simp`?
+  simp [List.foldlM_filterMap]
+  rfl
+
+theorem foldrM_filterMap [Monad m] [LawfulMonad m] (f : α → Option β) (g : β → γ → m γ) (l : Array α) (init : γ) :
+    (l.filterMap f).foldrM g init =
+      l.foldrM (fun x y => match f x with | some b => g b y | none => pure y) init := by
+  cases l
+  rw [List.filterMap_toArray] -- Why doesn't this fire via `simp`?
+  simp [List.foldrM_filterMap]
+  rfl
+
+theorem foldlM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : β → α → m β) (l : Array α) (init : β) :
+    (l.filter p).foldlM g init =
+      l.foldlM (fun x y => if p y then g x y else pure x) init := by
+  cases l
+  rw [List.filter_toArray] -- Why doesn't this fire via `simp`?
+  simp [List.foldlM_filter]
+
+theorem foldrM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : α → β → m β) (l : Array α) (init : β) :
+    (l.filter p).foldrM g init =
+      l.foldrM (fun x y => if p x then g x y else pure y) init := by
+  cases l
+  rw [List.filter_toArray] -- Why doesn't this fire via `simp`?
+  simp [List.foldrM_filter]
+
+/-! ### forIn' -/
+
+/--
+We can express a for loop over an array as a fold,
+in which whenever we reach `.done b` we keep that value through the rest of the fold.
+-/
+theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
+    (l : Array α) (f : (a : α) → a ∈ l → β → m (ForInStep β)) (init : β) :
+    forIn' l init f = ForInStep.value <$>
+      l.attach.foldlM (fun b ⟨a, m⟩ => match b with
+        | .yield b => f a m b
+        | .done b => pure (.done b)) (ForInStep.yield init) := by
+  cases l
+  rw [List.attach_toArray] -- Why doesn't this fire via `simp`?
+  simp only [List.forIn'_toArray, List.forIn'_eq_foldlM, List.attachWith_mem_toArray, size_toArray,
+    List.length_map, List.length_attach, List.foldlM_toArray', List.foldlM_map]
+  congr
+
+/-- We can express a for loop over an array which always yields as a fold. -/
+@[simp] theorem forIn'_yield_eq_foldlM [Monad m] [LawfulMonad m]
+    (l : Array α) (f : (a : α) → a ∈ l → β → m γ) (g : (a : α) → a ∈ l → β → γ → β) (init : β) :
+    forIn' l init (fun a m b => (fun c => .yield (g a m b c)) <$> f a m b) =
+      l.attach.foldlM (fun b ⟨a, m⟩ => g a m b <$> f a m b) init := by
+  cases l
+  rw [List.attach_toArray] -- Why doesn't this fire via `simp`?
+  simp [List.foldlM_map]
+
+theorem forIn'_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
+    (l : Array α) (f : (a : α) → a ∈ l → β → β) (init : β) :
+    forIn' l init (fun a m b => pure (.yield (f a m b))) =
+      pure (f := m) (l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init) := by
+  cases l
+  simp [List.forIn'_pure_yield_eq_foldl, List.foldl_map]
+
+@[simp] theorem forIn'_yield_eq_foldl
+    (l : Array α) (f : (a : α) → a ∈ l → β → β) (init : β) :
+    forIn' (m := Id) l init (fun a m b => .yield (f a m b)) =
+      l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init := by
+  cases l
+  simp [List.foldl_map]
+
+/--
+We can express a for loop over an array as a fold,
+in which whenever we reach `.done b` we keep that value through the rest of the fold.
+-/
+theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
+    (f : α → β → m (ForInStep β)) (init : β) (l : Array α) :
+    forIn l init f = ForInStep.value <$>
+      l.foldlM (fun b a => match b with
+        | .yield b => f a b
+        | .done b => pure (.done b)) (ForInStep.yield init) := by
+  cases l
+  simp only [List.forIn_toArray, List.forIn_eq_foldlM, size_toArray, List.foldlM_toArray']
+  congr
+
+/-- We can express a for loop over an array which always yields as a fold. -/
+@[simp] theorem forIn_yield_eq_foldlM [Monad m] [LawfulMonad m]
+    (l : Array α) (f : α → β → m γ) (g : α → β → γ → β) (init : β) :
+    forIn l init (fun a b => (fun c => .yield (g a b c)) <$> f a b) =
+      l.foldlM (fun b a => g a b <$> f a b) init := by
+  cases l
+  simp [List.foldlM_map]
+
+theorem forIn_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
+    (l : Array α) (f : α → β → β) (init : β) :
+    forIn l init (fun a b => pure (.yield (f a b))) =
+      pure (f := m) (l.foldl (fun b a => f a b) init) := by
+  cases l
+  simp [List.forIn_pure_yield_eq_foldl, List.foldl_map]
+
+@[simp] theorem forIn_yield_eq_foldl
+    (l : Array α) (f : α → β → β) (init : β) :
+    forIn (m := Id) l init (fun a b => .yield (f a b)) =
+      l.foldl (fun b a => f a b) init := by
+  cases l
+  simp [List.foldl_map]
+
+end Array

src/Init/Data/Array/Subarray.lean

@@ -15,15 +15,6 @@ structure Subarray (α : Type u)  where
   start_le_stop : start ≤ stop
   stop_le_array_size : stop ≤ array.size
 
-@[deprecated Subarray.array (since := "2024-04-13")]
-abbrev Subarray.as (s : Subarray α) : Array α := s.array
-
-@[deprecated Subarray.start_le_stop (since := "2024-04-13")]
-theorem Subarray.h₁ (s : Subarray α) : s.start ≤ s.stop := s.start_le_stop
-
-@[deprecated Subarray.stop_le_array_size (since := "2024-04-13")]
-theorem Subarray.h₂ (s : Subarray α) : s.stop ≤ s.array.size := s.stop_le_array_size
-
 namespace Subarray
 
 def size (s : Subarray α) : Nat :=

src/Init/Data/BitVec/Basic.lean

@@ -29,9 +29,6 @@ section Nat
 
 instance natCastInst : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩
 
-@[deprecated isLt (since := "2024-03-12")]
-theorem toNat_lt (x : BitVec n) : x.toNat < 2^n := x.isLt
-
 /-- Theorem for normalizing the bit vector literal representation. -/
 -- TODO: This needs more usage data to assess which direction the simp should go.
 @[simp, bv_toNat] theorem ofNat_eq_ofNat : @OfNat.ofNat (BitVec n) i _ = .ofNat n i := rfl

src/Init/Data/Fin/Lemmas.lean

@@ -642,7 +642,7 @@ theorem pred_add_one (i : Fin (n + 2)) (h : (i : Nat) < n + 1) :
   ext
   simp
 
-@[simp] theorem subNat_one_succ (i : Fin (n + 1)) (h : 1 ≤ ↑i) : (subNat 1 i h).succ = i := by
+@[simp] theorem subNat_one_succ (i : Fin (n + 1)) (h : 1 ≤ (i : Nat)) : (subNat 1 i h).succ = i := by
   ext
   simp
   omega

src/Init/Data/Float.lean

@@ -47,6 +47,25 @@ def Float.lt : Float → Float → Prop := fun a b =>
 def Float.le : Float → Float → Prop := fun a b =>
   floatSpec.le a.val b.val
 
+/--
+Raw transmutation from `UInt64`.
+
+Floats and UInts have the same endianness on all supported platforms.
+IEEE 754 very precisely specifies the bit layout of floats.
+-/
+@[extern "lean_float_from_bits"] opaque Float.fromBits : UInt64 → Float
+
+/--
+Raw transmutation to `UInt64`.
+
+Floats and UInts have the same endianness on all supported platforms.
+IEEE 754 very precisely specifies the bit layout of floats.
+
+Note that this function is distinct from `Float.toUInt64`, which attempts
+to preserve the numeric value, and not the bitwise value.
+-/
+@[extern "lean_float_to_bits"] opaque Float.toBits : Float → UInt64
+
 instance : Add Float := ⟨Float.add⟩
 instance : Sub Float := ⟨Float.sub⟩
 instance : Mul Float := ⟨Float.mul⟩

src/Init/Data/List/Basic.lean

@@ -551,7 +551,7 @@ theorem reverseAux_eq_append (as bs : List α) : reverseAux as bs = reverseAux a
 /-! ### flatten -/
 
 /--
-`O(|flatten L|)`. `join L` concatenates all the lists in `L` into one list.
+`O(|flatten L|)`. `flatten L` concatenates all the lists in `L` into one list.
 * `flatten [[a], [], [b, c], [d, e, f]] = [a, b, c, d, e, f]`
 -/
 def flatten : List (List α) → List α

src/Init/Data/List/Impl.lean

@@ -91,7 +91,7 @@ The following operations are given `@[csimp]` replacements below:
 @[specialize] def foldrTR (f : α → β → β) (init : β) (l : List α) : β := l.toArray.foldr f init
 
 @[csimp] theorem foldr_eq_foldrTR : @foldr = @foldrTR := by
-  funext α β f init l; simp [foldrTR, Array.foldr_eq_foldr_toList, -Array.size_toArray]
+  funext α β f init l; simp [foldrTR, ← Array.foldr_toList, -Array.size_toArray]
 
 /-! ### flatMap  -/
 
@@ -331,7 +331,7 @@ def enumFromTR (n : Nat) (l : List α) : List (Nat × α) :=
     | a::as, n => by
       rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., foldr, go as]
       simp [enumFrom, f]
-  rw [Array.foldr_eq_foldr_toList]
+  rw [← Array.foldr_toList]
   simp [go]
 
 /-! ## Other list operations -/

src/Init/Data/Nat/Linear.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.ByCases
 import Init.Data.Prod
+import Init.Data.RArray
 
 namespace Nat.Linear
 
@@ -15,7 +16,7 @@ namespace Nat.Linear
 
 abbrev Var := Nat
 
-abbrev Context := List Nat
+abbrev Context := Lean.RArray Nat
 
 /--
   When encoding polynomials. We use `fixedVar` for encoding numerals.
@@ -23,12 +24,7 @@ abbrev Context := List Nat
 def fixedVar := 100000000 -- Any big number should work here
 
 def Var.denote (ctx : Context) (v : Var) : Nat :=
-  bif v == fixedVar then 1 else go ctx v
-where
-  go : List Nat → Nat → Nat
-   | [],    _   => 0
-   | a::_,  0   => a
-   | _::as, i+1 => go as i
+  bif v == fixedVar then 1 else ctx.get v
 
 inductive Expr where
   | num  (v : Nat)
@@ -52,25 +48,23 @@ def Poly.denote (ctx : Context) (p : Poly) : Nat :=
   | [] => 0
   | (k, v) :: p => Nat.add (Nat.mul k (v.denote ctx)) (denote ctx p)
 
-def Poly.insertSorted (k : Nat) (v : Var) (p : Poly) : Poly :=
+def Poly.insert (k : Nat) (v : Var) (p : Poly) : Poly :=
   match p with
   | [] => [(k, v)]
-  | (k', v') :: p => bif Nat.blt v v' then (k, v) :: (k', v') :: p else (k', v') :: insertSorted k v p
+  | (k', v') :: p =>
+    bif Nat.blt v v' then
+      (k, v) :: (k', v') :: p
+    else bif Nat.beq v v' then
+      (k + k', v') :: p
+    else
+      (k', v') :: insert k v p
 
-def Poly.sort (p : Poly) : Poly :=
-  let rec go (p : Poly) (r : Poly) : Poly :=
+def Poly.norm (p : Poly) : Poly := go p []
+where
+  go (p : Poly) (r : Poly) : Poly :=
     match p with
     | [] => r
-    | (k, v) :: p => go p (r.insertSorted k v)
-  go p []
-
-def Poly.fuse (p : Poly) : Poly :=
-  match p with
-  | []  => []
-  | (k, v) :: p =>
-    match fuse p with
-    | [] => [(k, v)]
-    | (k', v') :: p' => bif v == v' then (Nat.add k k', v)::p' else (k, v) :: (k', v') :: p'
+    | (k, v) :: p => go p (r.insert k v)
 
 def Poly.mul (k : Nat) (p : Poly) : Poly :=
   bif k == 0 then
@@ -146,15 +140,17 @@ def Poly.combineAux (fuel : Nat) (p₁ p₂ : Poly) : Poly :=
 def Poly.combine (p₁ p₂ : Poly) : Poly :=
   combineAux hugeFuel p₁ p₂
 
-def Expr.toPoly : Expr → Poly
-  | Expr.num k    => bif k == 0 then [] else [ (k, fixedVar) ]
-  | Expr.var i    => [(1, i)]
-  | Expr.add a b  => a.toPoly ++ b.toPoly
-  | Expr.mulL k a => a.toPoly.mul k
-  | Expr.mulR a k => a.toPoly.mul k
-
-def Poly.norm (p : Poly) : Poly :=
-  p.sort.fuse
+def Expr.toPoly (e : Expr) :=
+  go 1 e []
+where
+  -- Implementation note: This assembles the result using difference lists
+  -- to avoid `++` on lists.
+  go (coeff : Nat) : Expr → (Poly → Poly)
+    | Expr.num k    => bif k == 0 then id else ((coeff * k, fixedVar) :: ·)
+    | Expr.var i    => ((coeff, i) :: ·)
+    | Expr.add a b  => go coeff a ∘ go coeff b
+    | Expr.mulL k a
+    | Expr.mulR a k => bif k == 0 then id else go (coeff * k) a
 
 def Expr.toNormPoly (e : Expr) : Poly :=
   e.toPoly.norm
@@ -201,7 +197,7 @@ def PolyCnstr.denote (ctx : Context) (c : PolyCnstr) : Prop :=
     Poly.denote_le ctx (c.lhs, c.rhs)
 
 def PolyCnstr.norm (c : PolyCnstr) : PolyCnstr :=
-  let (lhs, rhs) := Poly.cancel c.lhs.sort.fuse c.rhs.sort.fuse
+  let (lhs, rhs) := Poly.cancel c.lhs.norm c.rhs.norm
   { eq := c.eq, lhs, rhs }
 
 def PolyCnstr.isUnsat (c : PolyCnstr) : Bool :=
@@ -268,24 +264,32 @@ def PolyCnstr.toExpr (c : PolyCnstr) : ExprCnstr :=
   { c with lhs := c.lhs.toExpr, rhs := c.rhs.toExpr }
 
 attribute [local simp] Nat.add_comm Nat.add_assoc Nat.add_left_comm Nat.right_distrib Nat.left_distrib Nat.mul_assoc Nat.mul_comm
-attribute [local simp] Poly.denote Expr.denote Poly.insertSorted Poly.sort Poly.sort.go Poly.fuse Poly.cancelAux
+attribute [local simp] Poly.denote Expr.denote Poly.insert Poly.norm Poly.norm.go Poly.cancelAux
 attribute [local simp] Poly.mul Poly.mul.go
 
-theorem Poly.denote_insertSorted (ctx : Context) (k : Nat) (v : Var) (p : Poly) : (p.insertSorted k v).denote ctx = p.denote ctx + k * v.denote ctx := by
+theorem Poly.denote_insert (ctx : Context) (k : Nat) (v : Var) (p : Poly) :
+    (p.insert k v).denote ctx = p.denote ctx + k * v.denote ctx := by
   match p with
   | [] => simp
-  | (k', v') :: p => by_cases h : Nat.blt v v' <;> simp [h, denote_insertSorted]
+  | (k', v') :: p =>
+    by_cases h₁ : Nat.blt v v'
+    · simp [h₁]
+    · by_cases h₂ : Nat.beq v v'
+      · simp only [insert, h₁, h₂, cond_false, cond_true]
+        simp [Nat.eq_of_beq_eq_true h₂]
+      · simp only [insert, h₁, h₂, cond_false, cond_true]
+        simp [denote_insert]
 
-attribute [local simp] Poly.denote_insertSorted
+attribute [local simp] Poly.denote_insert
 
-theorem Poly.denote_sort_go (ctx : Context) (p : Poly) (r : Poly) : (sort.go p r).denote ctx = p.denote ctx + r.denote ctx := by
+theorem Poly.denote_norm_go (ctx : Context) (p : Poly) (r : Poly) : (norm.go p r).denote ctx = p.denote ctx + r.denote ctx := by
   match p with
   | [] => simp
-  | (k, v):: p => simp [denote_sort_go]
+  | (k, v):: p => simp [denote_norm_go]
 
-attribute [local simp] Poly.denote_sort_go
+attribute [local simp] Poly.denote_norm_go
 
-theorem Poly.denote_sort (ctx : Context) (m : Poly) : m.sort.denote ctx = m.denote ctx := by
+theorem Poly.denote_sort (ctx : Context) (m : Poly) : m.norm.denote ctx = m.denote ctx := by
   simp
 
 attribute [local simp] Poly.denote_sort
@@ -316,18 +320,6 @@ theorem Poly.denote_reverse (ctx : Context) (p : Poly) : denote ctx (List.revers
 
 attribute [local simp] Poly.denote_reverse
 
-theorem Poly.denote_fuse (ctx : Context) (p : Poly) : p.fuse.denote ctx = p.denote ctx := by
-  match p with
-  | [] => rfl
-  | (k, v) :: p =>
-    have ih := denote_fuse ctx p
-    simp
-    split
-    case _ h => simp [← ih, h]
-    case _ k' v' p' h => by_cases he : v == v' <;> simp [he, ← ih, h]; rw [eq_of_beq he]
-
-attribute [local simp] Poly.denote_fuse
-
 theorem Poly.denote_mul (ctx : Context) (k : Nat) (p : Poly) : (p.mul k).denote ctx = k * p.denote ctx := by
   simp
   by_cases h : k == 0 <;> simp [h]; simp [eq_of_beq h]
@@ -516,13 +508,25 @@ theorem Poly.denote_combine (ctx : Context) (p₁ p₂ : Poly) : (p₁.combine p
 
 attribute [local simp] Poly.denote_combine
 
+theorem Expr.denote_toPoly_go (ctx : Context) (e : Expr) :
+  (toPoly.go k e p).denote ctx = k * e.denote ctx + p.denote ctx := by
+  induction k, e using Expr.toPoly.go.induct generalizing p with
+  | case1 k k' =>
+    simp only [toPoly.go]
+    by_cases h : k' == 0
+    · simp [h, eq_of_beq h]
+    · simp [h, Var.denote]
+  | case2 k i => simp [toPoly.go]
+  | case3 k a b iha ihb => simp [toPoly.go, iha, ihb]
+  | case4 k k' a ih
+  | case5 k a k' ih =>
+    simp only [toPoly.go, denote, mul_eq]
+    by_cases h : k' == 0
+    · simp [h, eq_of_beq h]
+    · simp [h, cond_false, ih, Nat.mul_assoc]
+
 theorem Expr.denote_toPoly (ctx : Context) (e : Expr) : e.toPoly.denote ctx = e.denote ctx := by
-  induction e with
-  | num k => by_cases h : k == 0 <;> simp [toPoly, h, Var.denote]; simp [eq_of_beq h]
-  | var i => simp [toPoly]
-  | add a b iha ihb => simp [toPoly, iha, ihb]
-  | mulL k a ih => simp [toPoly, ih, -Poly.mul]
-  | mulR k a ih => simp [toPoly, ih, -Poly.mul]
+  simp [toPoly, Expr.denote_toPoly_go]
 
 attribute [local simp] Expr.denote_toPoly
 
@@ -554,8 +558,8 @@ theorem ExprCnstr.denote_toPoly (ctx : Context) (c : ExprCnstr) : c.toPoly.denot
   cases c; rename_i eq lhs rhs
   simp [ExprCnstr.denote, PolyCnstr.denote, ExprCnstr.toPoly];
   by_cases h : eq = true <;> simp [h]
-  · simp [Poly.denote_eq, Expr.toPoly]
-  · simp [Poly.denote_le, Expr.toPoly]
+  · simp [Poly.denote_eq]
+  · simp [Poly.denote_le]
 
 attribute [local simp] ExprCnstr.denote_toPoly
 

src/Init/Data/Option/Basic.lean

@@ -16,10 +16,6 @@ def getM [Alternative m] : Option α → m α
   | none     => failure
   | some a   => pure a
 
-@[deprecated getM (since := "2024-04-17")]
--- `[Monad m]` is not needed here.
-def toMonad [Monad m] [Alternative m] : Option α → m α := getM
-
 /-- Returns `true` on `some x` and `false` on `none`. -/
 @[inline] def isSome : Option α → Bool
   | some _ => true
@@ -28,8 +24,6 @@ def toMonad [Monad m] [Alternative m] : Option α → m α := getM
 @[simp] theorem isSome_none : @isSome α none = false := rfl
 @[simp] theorem isSome_some : isSome (some a) = true := rfl
 
-@[deprecated isSome (since := "2024-04-17"), inline] def toBool : Option α → Bool := isSome
-
 /-- Returns `true` on `none` and `false` on `some x`. -/
 @[inline] def isNone : Option α → Bool
   | some _ => false

src/Init/Data/RArray.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+
+prelude
+import Init.PropLemmas
+
+namespace Lean
+
+/--
+A `RArray` can model `Fin n → α` or `Array α`, but is optimized for a fast kernel-reducible `get`
+operation.
+
+The primary intended use case is the “denote” function of a typical proof by reflection proof, where
+only the `get` operation is necessary. It is not suitable as a general-purpose data structure.
+
+There is no well-formedness invariant attached to this data structure, to keep it concise; it's
+semantics is given through `RArray.get`. In that way one can also view an `RArray` as a decision
+tree implementing `Nat → α`.
+
+See `RArray.ofFn` and `RArray.ofArray` in module `Lean.Data.RArray` for functions that construct an
+`RArray`.
+
+It is not universe-polymorphic. ; smaller proof objects and no complication with the `ToExpr` type
+class.
+-/
+inductive RArray (α : Type) : Type where
+  | leaf : α → RArray α
+  | branch : Nat → RArray α → RArray α → RArray α
+
+variable {α : Type}
+
+/-- The crucial operation, written with very little abstractional overhead -/
+noncomputable def RArray.get (a : RArray α) (n : Nat) : α :=
+  RArray.rec (fun x => x) (fun p _ _ l r => (Nat.ble p n).rec l r) a
+
+private theorem RArray.get_eq_def (a : RArray α) (n : Nat) :
+  a.get n = match a with
+    | .leaf x => x
+    | .branch p l r => (Nat.ble p n).rec (l.get n) (r.get n) := by
+  conv => lhs; unfold RArray.get
+  split <;> rfl
+
+/-- `RArray.get`, implemented conventionally -/
+def RArray.getImpl (a : RArray α) (n : Nat) : α :=
+  match a with
+  | .leaf x => x
+  | .branch p l r => if n < p then l.getImpl n else r.getImpl n
+
+@[csimp]
+theorem RArray.get_eq_getImpl : @RArray.get = @RArray.getImpl := by
+  funext α a n
+  induction a with
+  | leaf _ => rfl
+  | branch p l r ihl ihr =>
+    rw [RArray.getImpl, RArray.get_eq_def]
+    simp only [ihl, ihr, ← Nat.not_le, ← Nat.ble_eq, ite_not]
+    cases hnp : Nat.ble p n <;> rfl
+
+instance : GetElem (RArray α) Nat α (fun _ _ => True) where
+  getElem a n _ := a.get n
+
+def RArray.size : RArray α → Nat
+  | leaf _ => 1
+  | branch _ l r => l.size + r.size
+
+end Lean

src/Init/Data/SInt/Basic.lean

@@ -148,6 +148,9 @@ instance : ShiftLeft Int8   := ⟨Int8.shiftLeft⟩
 instance : ShiftRight Int8  := ⟨Int8.shiftRight⟩
 instance : DecidableEq Int8 := Int8.decEq
 
+@[extern "lean_bool_to_int8"]
+def Bool.toInt8 (b : Bool) : Int8 := if b then 1 else 0
+
 @[extern "lean_int8_dec_lt"]
 def Int8.decLt (a b : Int8) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
@@ -249,6 +252,9 @@ instance : ShiftLeft Int16   := ⟨Int16.shiftLeft⟩
 instance : ShiftRight Int16  := ⟨Int16.shiftRight⟩
 instance : DecidableEq Int16 := Int16.decEq
 
+@[extern "lean_bool_to_int16"]
+def Bool.toInt16 (b : Bool) : Int16 := if b then 1 else 0
+
 @[extern "lean_int16_dec_lt"]
 def Int16.decLt (a b : Int16) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
@@ -354,6 +360,9 @@ instance : ShiftLeft Int32   := ⟨Int32.shiftLeft⟩
 instance : ShiftRight Int32  := ⟨Int32.shiftRight⟩
 instance : DecidableEq Int32 := Int32.decEq
 
+@[extern "lean_bool_to_int32"]
+def Bool.toInt32 (b : Bool) : Int32 := if b then 1 else 0
+
 @[extern "lean_int32_dec_lt"]
 def Int32.decLt (a b : Int32) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
@@ -463,6 +472,9 @@ instance : ShiftLeft Int64   := ⟨Int64.shiftLeft⟩
 instance : ShiftRight Int64  := ⟨Int64.shiftRight⟩
 instance : DecidableEq Int64 := Int64.decEq
 
+@[extern "lean_bool_to_int64"]
+def Bool.toInt64 (b : Bool) : Int64 := if b then 1 else 0
+
 @[extern "lean_int64_dec_lt"]
 def Int64.decLt (a b : Int64) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))
@@ -574,6 +586,9 @@ instance : ShiftLeft ISize   := ⟨ISize.shiftLeft⟩
 instance : ShiftRight ISize  := ⟨ISize.shiftRight⟩
 instance : DecidableEq ISize := ISize.decEq
 
+@[extern "lean_bool_to_isize"]
+def Bool.toISize (b : Bool) : ISize := if b then 1 else 0
+
 @[extern "lean_isize_dec_lt"]
 def ISize.decLt (a b : ISize) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec.slt b.toBitVec))

src/Init/Data/String/Basic.lean

@@ -514,9 +514,6 @@ instance : Inhabited String := ⟨""⟩
 
 instance : Append String := ⟨String.append⟩
 
-@[deprecated push (since := "2024-04-06")]
-def str : String → Char → String := push
-
 @[inline] def pushn (s : String) (c : Char) (n : Nat) : String :=
   n.repeat (fun s => s.push c) s
 

src/Init/Data/UInt/Basic.lean

@@ -56,6 +56,9 @@ instance : Xor UInt8       := ⟨UInt8.xor⟩
 instance : ShiftLeft UInt8  := ⟨UInt8.shiftLeft⟩
 instance : ShiftRight UInt8 := ⟨UInt8.shiftRight⟩
 
+@[extern "lean_bool_to_uint8"]
+def Bool.toUInt8 (b : Bool) : UInt8 := if b then 1 else 0
+
 @[extern "lean_uint8_dec_lt"]
 def UInt8.decLt (a b : UInt8) : Decidable (a < b) :=
   inferInstanceAs (Decidable (a.toBitVec < b.toBitVec))
@@ -116,6 +119,9 @@ instance : Xor UInt16       := ⟨UInt16.xor⟩
 instance : ShiftLeft UInt16  := ⟨UInt16.shiftLeft⟩
 instance : ShiftRight UInt16 := ⟨UInt16.shiftRight⟩
 
+@[extern "lean_bool_to_uint16"]
+def Bool.toUInt16 (b : Bool) : UInt16 := if b then 1 else 0
+
 set_option bootstrap.genMatcherCode false in
 @[extern "lean_uint16_dec_lt"]
 def UInt16.decLt (a b : UInt16) : Decidable (a < b) :=
@@ -174,6 +180,9 @@ instance : Xor UInt32       := ⟨UInt32.xor⟩
 instance : ShiftLeft UInt32  := ⟨UInt32.shiftLeft⟩
 instance : ShiftRight UInt32 := ⟨UInt32.shiftRight⟩
 
+@[extern "lean_bool_to_uint32"]
+def Bool.toUInt32 (b : Bool) : UInt32 := if b then 1 else 0
+
 @[extern "lean_uint64_add"]
 def UInt64.add (a b : UInt64) : UInt64 := ⟨a.toBitVec + b.toBitVec⟩
 @[extern "lean_uint64_sub"]
@@ -278,5 +287,8 @@ instance : Xor USize        := ⟨USize.xor⟩
 instance : ShiftLeft USize  := ⟨USize.shiftLeft⟩
 instance : ShiftRight USize := ⟨USize.shiftRight⟩
 
+@[extern "lean_bool_to_usize"]
+def Bool.toUSize (b : Bool) : USize := if b then 1 else 0
+
 instance : Max USize := maxOfLe
 instance : Min USize := minOfLe

src/Init/Prelude.lean

@@ -2829,17 +2829,6 @@ instance {α : Type u} {m : Type u → Type v} [Monad m] [Inhabited α] : Inhabi
 instance [Monad m] : [Nonempty α] → Nonempty (m α)
   | ⟨x⟩ => ⟨pure x⟩
 
-/-- A fusion of Haskell's `sequence` and `map`. Used in syntax quotations. -/
-def Array.sequenceMap {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : α → m β) : m (Array β) :=
-  let rec loop (i : Nat) (j : Nat) (bs : Array β) : m (Array β) :=
-    dite (LT.lt j as.size)
-      (fun hlt =>
-        match i with
-        | 0           => pure bs
-        | Nat.succ i' => Bind.bind (f (as.get j hlt)) fun b => loop i' (hAdd j 1) (bs.push b))
-      (fun _ => pure bs)
-  loop as.size 0 (Array.mkEmpty as.size)
-
 /--
 A function for lifting a computation from an inner `Monad` to an outer `Monad`.
 Like Haskell's [`MonadTrans`], but `n` does not have to be a monad transformer.

src/Init/Tactics.lean

@@ -466,7 +466,7 @@ hypotheses or the goal. It can have one of the forms:
 * `at h₁ h₂ ⊢`: target the hypotheses `h₁` and `h₂`, and the goal
 * `at *`: target all hypotheses and the goal
 -/
-syntax location := withPosition(" at" (locationWildcard <|> locationHyp))
+syntax location := withPosition(ppGroup(" at" (locationWildcard <|> locationHyp)))
 
 /--
 * `change tgt'` will change the goal from `tgt` to `tgt'`,

src/Lean/Compiler/ConstFolding.lean

@@ -133,8 +133,8 @@ def foldNatBinBoolPred (fn : Nat → Nat → Bool) (a₁ a₂ : Expr) : Option E
     return mkConst ``Bool.false
 
 def foldNatBeq := fun _ : Bool => foldNatBinBoolPred (fun a b => a == b)
-def foldNatBle := fun _ : Bool => foldNatBinBoolPred (fun a b => a < b)
-def foldNatBlt := fun _ : Bool => foldNatBinBoolPred (fun a b => a ≤ b)
+def foldNatBlt := fun _ : Bool => foldNatBinBoolPred (fun a b => a < b)
+def foldNatBle := fun _ : Bool => foldNatBinBoolPred (fun a b => a ≤ b)
 
 def natFoldFns : List (Name × BinFoldFn) :=
   [(``Nat.add, foldNatAdd),

src/Lean/Data.lean

@@ -29,4 +29,4 @@ import Lean.Data.Xml
 import Lean.Data.NameTrie
 import Lean.Data.RBTree
 import Lean.Data.RBMap
-import Lean.Data.Rat
+import Lean.Data.RArray

src/Lean/Data/NameMap.lean

@@ -33,6 +33,16 @@ def find? (m : NameMap α) (n : Name) : Option α := RBMap.find? m n
 instance : ForIn m (NameMap α) (Name × α) :=
   inferInstanceAs (ForIn _ (RBMap ..) ..)
 
+/-- `filter f m` returns the `NameMap` consisting of all
+"`key`/`val`"-pairs in `m` where `f key val` returns `true`. -/
+def filter (f : Name → α → Bool) (m : NameMap α) : NameMap α := RBMap.filter f m
+
+/-- `filterMap f m` filters an `NameMap` and simultaneously modifies the filtered values.
+
+It takes a function `f : Name → α → Option β` and applies `f name` to the value with key `name`.
+The resulting entries with non-`none` value are collected to form the output `NameMap`. -/
+def filterMap (f : Name → α → Option β) (m : NameMap α) : NameMap β := RBMap.filterMap f m
+
 end NameMap
 
 def NameSet := RBTree Name Name.quickCmp
@@ -53,6 +63,9 @@ def append (s t : NameSet) : NameSet :=
 instance : Append NameSet where
   append := NameSet.append
 
+/-- `filter f s` returns the `NameSet` consisting of all `x` in `s` where `f x` returns `true`. -/
+def filter (f : Name → Bool) (s : NameSet) : NameSet := RBTree.filter f s
+
 end NameSet
 
 def NameSSet := SSet Name
@@ -73,6 +86,9 @@ instance : EmptyCollection NameHashSet := ⟨empty⟩
 instance : Inhabited NameHashSet := ⟨{}⟩
 def insert (s : NameHashSet) (n : Name) := Std.HashSet.insert s n
 def contains (s : NameHashSet) (n : Name) : Bool := Std.HashSet.contains s n
+
+/-- `filter f s` returns the `NameHashSet` consisting of all `x` in `s` where `f x` returns `true`. -/
+def filter (f : Name → Bool) (s : NameHashSet) : NameHashSet := Std.HashSet.filter f s
 end NameHashSet
 
 def MacroScopesView.isPrefixOf (v₁ v₂ : MacroScopesView) : Bool :=

src/Lean/Data/RArray.lean

@@ -0,0 +1,75 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+
+prelude
+import Init.Data.RArray
+import Lean.ToExpr
+
+/-!
+Auxillary definitions related to `Lean.RArray` that are typically only used in meta-code, in
+particular the `ToExpr` instance.
+-/
+
+namespace Lean
+
+-- This function could live in Init/Data/RArray.lean, but without omega it's tedious to implement
+def RArray.ofFn {n : Nat} (f : Fin n → α) (h : 0 < n) : RArray α :=
+  go 0 n h (Nat.le_refl _)
+where
+  go (lb ub : Nat) (h1 : lb < ub) (h2 : ub ≤ n) : RArray α :=
+    if h : lb + 1 = ub then
+      .leaf (f ⟨lb, Nat.lt_of_lt_of_le h1 h2⟩)
+    else
+      let mid := (lb + ub)/2
+      .branch mid (go lb mid (by omega) (by omega)) (go mid ub (by omega) h2)
+
+def RArray.ofArray (xs : Array α) (h : 0 < xs.size) : RArray α :=
+  .ofFn (xs[·]) h
+
+/-- The correctness theorem for `ofFn` -/
+theorem RArray.get_ofFn {n : Nat} (f : Fin n → α) (h : 0 < n) (i : Fin n) :
+    (ofFn f h).get i = f i :=
+  go 0 n h (Nat.le_refl _) (Nat.zero_le _) i.2
+where
+  go lb ub h1 h2 (h3 : lb ≤ i.val) (h3 : i.val < ub) : (ofFn.go f lb ub h1 h2).get i = f i := by
+    induction lb, ub, h1, h2 using RArray.ofFn.go.induct (f := f) (n := n)
+    case case1 =>
+      simp [ofFn.go, RArray.get_eq_getImpl, RArray.getImpl]
+      congr
+      omega
+    case case2 ih1 ih2 hiu =>
+      rw [ofFn.go]; simp only [↓reduceDIte, *]
+      simp [RArray.get_eq_getImpl, RArray.getImpl] at *
+      split
+      · rw [ih1] <;> omega
+      · rw [ih2] <;> omega
+
+@[simp]
+theorem RArray.size_ofFn {n : Nat} (f : Fin n → α) (h : 0 < n) :
+    (ofFn f h).size = n :=
+  go 0 n h (Nat.le_refl _)
+where
+  go lb ub h1 h2 : (ofFn.go f lb ub h1 h2).size = ub - lb := by
+    induction lb, ub, h1, h2 using RArray.ofFn.go.induct (f := f) (n := n)
+    case case1 => simp [ofFn.go, size]; omega
+    case case2 ih1 ih2 hiu => rw [ofFn.go]; simp [size, *]; omega
+
+section Meta
+open Lean
+
+def RArray.toExpr (ty : Expr) (f : α → Expr) : RArray α → Expr
+  | .leaf x  =>
+    mkApp2 (mkConst ``RArray.leaf) ty (f x)
+  | .branch p l r =>
+    mkApp4 (mkConst ``RArray.branch) ty (mkRawNatLit p) (l.toExpr ty f) (r.toExpr ty f)
+
+instance [ToExpr α] : ToExpr (RArray α) where
+  toTypeExpr := mkApp (mkConst ``RArray) (toTypeExpr α)
+  toExpr a := a.toExpr (toTypeExpr α) toExpr
+
+end Meta
+
+end Lean

src/Lean/Data/RBMap.lean

@@ -404,6 +404,24 @@ def intersectBy {γ : Type v₁} {δ : Type v₂} (mergeFn : α → β → γ
       | some b₂ => acc.insert a <| mergeFn a b₁ b₂
       | none => acc
 
+/--
+`filter f m` returns the `RBMap` consisting of all
+"`key`/`val`"-pairs in `m` where `f key val` returns `true`.
+-/
+def filter (f : α → β → Bool) (m : RBMap α β cmp) : RBMap α β cmp :=
+  m.fold (fun r k v => if f k v then r.insert k v else r) {}
+
+/--
+`filterMap f m` filters an `RBMap` and simultaneously modifies the filtered values.
+
+It takes a function `f : α → β → Option γ` and applies `f k v` to the value with key `k`.
+The resulting entries with non-`none` value are collected to form the output `RBMap`.
+-/
+def filterMap (f : α → β → Option γ) (m : RBMap α β cmp) : RBMap α γ cmp :=
+  m.fold (fun r k v => match f k v with
+    | none => r
+    | some b => r.insert k b) {}
+
 end RBMap
 
 def rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (cmp : α → α → Ordering) : RBMap α β cmp :=

src/Lean/Data/RBTree.lean

@@ -114,6 +114,13 @@ def union (t₁ t₂ : RBTree α cmp) : RBTree α cmp :=
 def diff (t₁ t₂ : RBTree α cmp) : RBTree α cmp :=
   t₂.fold .erase t₁
 
+/--
+`filter f m` returns the `RBTree` consisting of all
+`x` in `m` where `f x` returns `true`.
+-/
+def filter (f : α → Bool) (m : RBTree α cmp) : RBTree α cmp :=
+  RBMap.filter (fun a _ => f a) m
+
 end RBTree
 
 def rbtreeOf {α : Type u} (l : List α) (cmp : α → α → Ordering) : RBTree α cmp :=

src/Lean/Elab/Command.lean

@@ -214,7 +214,7 @@ private def addTraceAsMessagesCore (ctx : Context) (log : MessageLog) (traceStat
   let mut log := log
   let traces' := traces.toArray.qsort fun ((a, _), _) ((b, _), _) => a < b
   for ((pos, endPos), traceMsg) in traces' do
-    let data := .tagged `_traceMsg <| .joinSep traceMsg.toList "\n"
+    let data := .tagged `trace <| .joinSep traceMsg.toList "\n"
     log := log.add <| mkMessageCore ctx.fileName ctx.fileMap data .information pos endPos
   return log
 

src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean

@@ -50,7 +50,9 @@ private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
         go mvarId
       else if let some mvarId ← whnfReducibleLHS? mvarId then
         go mvarId
-      else match (← simpTargetStar mvarId { config.dsimp := false } (simprocs := {})).1 with
+      else
+        let ctx ← Simp.mkContext (config := { dsimp := false })
+        match (← simpTargetStar mvarId ctx (simprocs := {})).1 with
         | TacticResultCNM.closed => return ()
         | TacticResultCNM.modified mvarId => go mvarId
         | TacticResultCNM.noChange =>

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -45,7 +45,9 @@ where
       go mvarId
     else if let some mvarId ← simpIf? mvarId then
       go mvarId
-    else match (← simpTargetStar mvarId {} (simprocs := {})).1 with
+    else
+      let ctx ← Simp.mkContext
+      match (← simpTargetStar mvarId ctx (simprocs := {})).1 with
       | TacticResultCNM.closed => return ()
       | TacticResultCNM.modified mvarId => go mvarId
       | TacticResultCNM.noChange =>

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -57,7 +57,9 @@ private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
         go mvarId
       else if let some mvarId ← whnfReducibleLHS? mvarId then
         go mvarId
-      else match (← simpTargetStar mvarId { config.dsimp := false } (simprocs := {})).1 with
+      else
+        let ctx ← Simp.mkContext (config := { dsimp := false })
+        match (← simpTargetStar mvarId ctx (simprocs := {})).1 with
         | TacticResultCNM.closed => return ()
         | TacticResultCNM.modified mvarId => go mvarId
         | TacticResultCNM.noChange =>

src/Lean/Elab/PreDefinition/WF/Fix.lean

@@ -227,7 +227,7 @@ def mkFix (preDef : PreDefinition) (prefixArgs : Array Expr) (argsPacker : ArgsP
     -- decreasing goals when the function has only one non fixed argument.
     -- This renaming is irrelevant if the function has multiple non fixed arguments. See `process*` functions above.
     let lctx := (← getLCtx).setUserName x.fvarId! varName
-    withTheReader Meta.Context (fun ctx => { ctx with lctx }) do
+    withLCtx' lctx do
       let F   := xs[1]!
       let val := preDef.value.beta (prefixArgs.push x)
       let val ← processSumCasesOn x F val fun x F val => do

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -166,7 +166,7 @@ def mayOmitSizeOf (is_mutual : Bool) (args : Array Expr) (x : Expr) : MetaM Bool
 def withUserNames {α} (xs : Array Expr) (ns : Array Name) (k : MetaM α) : MetaM α := do
   let mut lctx ←  getLCtx
   for x in xs, n in ns do lctx := lctx.setUserName x.fvarId! n
-  withTheReader Meta.Context (fun ctx => { ctx with lctx }) k
+  withLCtx' lctx k
 
 /-- Create one measure for each (eligible) parameter of the given predefintion.  -/
 def simpleMeasures (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)

src/Lean/Elab/PreDefinition/WF/Main.lean

@@ -87,7 +87,7 @@ def varyingVarNames (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Ar
     xs.mapM (·.fvarId!.getUserName)
 
 def wfRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Option TerminationArgument)) : TermElabM Unit := do
-  let termArgs? := termArg?s.sequenceMap id -- Either all or none, checked by `elabTerminationByHints`
+  let termArgs? := termArg?s.mapM id -- Either all or none, checked by `elabTerminationByHints`
   let preDefs ← preDefs.mapM fun preDef =>
     return { preDef with value := (← preprocess preDef.value) }
   let (fixedPrefixSize, argsPacker, unaryPreDef) ← withoutModifyingEnv do

src/Lean/Elab/Quotation.lean

@@ -434,7 +434,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
             else mkNullNode contents
           -- We use `no_error_if_unused%` in auxiliary `match`-syntax to avoid spurious error messages,
           -- the outer `match` is checking for unused alternatives
-          `(match ($(discrs).sequenceMap fun
+          `(match ($(discrs).mapM fun
                 | `($contents) => no_error_if_unused% some $tuple
                 | _            => no_error_if_unused% none) with
               | some $resId => $yes

src/Lean/Elab/Syntax.lean

@@ -233,11 +233,14 @@ where
     return (← `((with_annotate_term $(stx[0]) @ParserDescr.sepBy1) $p $sep $psep $(quote allowTrailingSep)), 1)
 
   isValidAtom (s : String) : Bool :=
+    -- Pretty-printing instructions shouldn't affect validity
+    let s := s.trim
     !s.isEmpty &&
-    s.front != '\'' &&
+    (s.front != '\'' || s == "''") &&
     s.front != '\"' &&
     !(s.front == '`' && (s.endPos == ⟨1⟩ || isIdFirst (s.get ⟨1⟩) || isIdBeginEscape (s.get ⟨1⟩))) &&
-    !s.front.isDigit
+    !s.front.isDigit &&
+    !(s.any Char.isWhitespace)
 
   processAtom (stx : Syntax) := do
     match stx[0].isStrLit? with

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean

@@ -198,11 +198,10 @@ def rewriteRulesPass (maxSteps : Nat) : Pass where
     let sevalThms ← getSEvalTheorems
     let sevalSimprocs ← Simp.getSEvalSimprocs
 
-    let simpCtx : Simp.Context := {
-      config := { failIfUnchanged := false, zetaDelta := true, maxSteps }
-      simpTheorems := #[bvThms, sevalThms]
-      congrTheorems := (← getSimpCongrTheorems)
-    }
+    let simpCtx ← Simp.mkContext
+      (config := { failIfUnchanged := false, zetaDelta := true, maxSteps })
+      (simpTheorems := #[bvThms, sevalThms])
+      (congrTheorems := (← getSimpCongrTheorems))
 
     let hyps ← goal.getNondepPropHyps
     let ⟨result?, _⟩ ← simpGoal goal
@@ -217,35 +216,23 @@ Flatten out ands. That is look for hypotheses of the form `h : (x && y) = true`
 with `h.left : x = true` and `h.right : y = true`. This can enable more fine grained substitutions
 in embedded constraint substitution.
 -/
-def andFlatteningPass : Pass where
+partial def andFlatteningPass : Pass where
   name := `andFlattening
   run goal := do
     goal.withContext do
       let hyps ← goal.getNondepPropHyps
       let mut newHyps := #[]
       let mut oldHyps := #[]
-      for hyp in hyps do
-        let typ ← hyp.getType
-        let_expr Eq α eqLhs eqRhs := typ | continue
-        let_expr Bool.and lhs rhs := eqLhs | continue
-        let_expr Bool := α | continue
-        let_expr Bool.true := eqRhs | continue
-        let mkEqTrue (lhs : Expr) : Expr :=
-          mkApp3 (mkConst ``Eq [1]) (mkConst ``Bool) lhs (mkConst ``Bool.true)
-        let hypExpr := (← hyp.getDecl).toExpr
-        let leftHyp : Hypothesis := {
-          userName := (← hyp.getUserName) ++ `left,
-          type := mkEqTrue lhs,
-          value := mkApp3 (mkConst ``Std.Tactic.BVDecide.Normalize.Bool.and_left) lhs rhs hypExpr
+      for fvar in hyps do
+        let hyp : Hypothesis := {
+          userName := (← fvar.getDecl).userName
+          type := ← fvar.getType
+          value := mkFVar fvar
         }
-        let rightHyp : Hypothesis := {
-          userName := (← hyp.getUserName) ++ `right,
-          type := mkEqTrue rhs,
-          value := mkApp3 (mkConst ``Std.Tactic.BVDecide.Normalize.Bool.and_right) lhs rhs hypExpr
-        }
-        newHyps := newHyps.push leftHyp
-        newHyps := newHyps.push rightHyp
-        oldHyps := oldHyps.push hyp
+        let sizeBefore := newHyps.size
+        newHyps ← splitAnds hyp newHyps
+        if newHyps.size > sizeBefore then
+          oldHyps := oldHyps.push fvar
       if newHyps.size == 0 then
         return goal
       else
@@ -253,6 +240,38 @@ def andFlatteningPass : Pass where
         -- Given that we collected the hypotheses in the correct order above the invariant is given
         let goal ← goal.tryClearMany oldHyps
         return goal
+where
+  splitAnds (hyp : Hypothesis) (hyps : Array Hypothesis) (first : Bool := true) :
+      MetaM (Array Hypothesis) := do
+    match ← trySplit hyp with
+    | some (left, right) =>
+      let hyps ← splitAnds left hyps false
+      splitAnds right hyps false
+    | none =>
+      if first then
+        return hyps
+      else
+        return hyps.push hyp
+
+  trySplit (hyp : Hypothesis) : MetaM (Option (Hypothesis × Hypothesis)) := do
+    let typ := hyp.type
+    let_expr Eq α eqLhs eqRhs := typ | return none
+    let_expr Bool.and lhs rhs := eqLhs | return none
+    let_expr Bool.true := eqRhs | return none
+    let_expr Bool := α | return none
+    let mkEqTrue (lhs : Expr) : Expr :=
+      mkApp3 (mkConst ``Eq [1]) (mkConst ``Bool) lhs (mkConst ``Bool.true)
+    let leftHyp : Hypothesis := {
+      userName := hyp.userName,
+      type := mkEqTrue lhs,
+      value := mkApp3 (mkConst ``Std.Tactic.BVDecide.Normalize.Bool.and_left) lhs rhs hyp.value
+    }
+    let rightHyp : Hypothesis := {
+      userName := hyp.userName,
+      type := mkEqTrue rhs,
+      value := mkApp3 (mkConst ``Std.Tactic.BVDecide.Normalize.Bool.and_right) lhs rhs hyp.value
+    }
+    return some (leftHyp, rightHyp)
 
 /--
 Substitute embedded constraints. That is look for hypotheses of the form `h : x = true` and use
@@ -283,11 +302,10 @@ def embeddedConstraintPass (maxSteps : Nat) : Pass where
 
       let goal ← goal.tryClearMany duplicates
 
-      let simpCtx : Simp.Context := {
-        config := { failIfUnchanged := false, maxSteps }
-        simpTheorems := relevantHyps
-        congrTheorems := (← getSimpCongrTheorems)
-      }
+      let simpCtx ← Simp.mkContext
+        (config := { failIfUnchanged := false, maxSteps })
+        (simpTheorems := relevantHyps)
+        (congrTheorems := (← getSimpCongrTheorems))
 
       let ⟨result?, _⟩ ← simpGoal goal (ctx := simpCtx) (fvarIdsToSimp := ← goal.getNondepPropHyps)
       let some (_, newGoal) := result? | return none
@@ -310,22 +328,18 @@ def acNormalizePass : Pass where
 
     return newGoal
 
-/--
-The normalization passes used by `bv_normalize` and thus `bv_decide`.
--/
-def defaultPipeline (cfg : BVDecideConfig ): List Pass :=
-  [
-    rewriteRulesPass cfg.maxSteps,
-    andFlatteningPass,
-    embeddedConstraintPass cfg.maxSteps
-  ]
-
 def passPipeline (cfg : BVDecideConfig) : List Pass := Id.run do
-  let mut passPipeline := defaultPipeline cfg
+  let mut passPipeline := [rewriteRulesPass cfg.maxSteps]
 
   if cfg.acNf then
     passPipeline := passPipeline ++ [acNormalizePass]
 
+  if cfg.andFlattening then
+    passPipeline := passPipeline ++ [andFlatteningPass]
+
+  if cfg.embeddedConstraintSubst then
+    passPipeline := passPipeline ++ [embeddedConstraintPass cfg.maxSteps]
+
   return passPipeline
 
 end Pass

src/Lean/Elab/Tactic/Conv/Pattern.lean

@@ -12,11 +12,10 @@ namespace Lean.Elab.Tactic.Conv
 open Meta
 
 private def getContext : MetaM Simp.Context := do
-  return {
-    simpTheorems  := {}
-    congrTheorems := (← getSimpCongrTheorems)
-    config        := Simp.neutralConfig
-  }
+  Simp.mkContext
+    (simpTheorems  := {})
+    (congrTheorems := (← getSimpCongrTheorems))
+    (config        := Simp.neutralConfig)
 
 partial def matchPattern? (pattern : AbstractMVarsResult) (e : Expr) : MetaM (Option (Expr × Array Expr)) :=
   withNewMCtxDepth do
@@ -126,7 +125,7 @@ private def pre (pattern : AbstractMVarsResult) (state : IO.Ref PatternMatchStat
         pure (.occs #[] 0 ids.toList)
       | _ => throwUnsupportedSyntax
     let state ← IO.mkRef occs
-    let ctx := { ← getContext with config.memoize := occs matches .all _ }
+    let ctx := (← getContext).setMemoize (occs matches .all _)
     let (result, _) ← Simp.main lhs ctx (methods := { pre := pre patternA state })
     let subgoals ← match ← state.get with
     | .all #[] | .occs _ 0 _ =>

src/Lean/Elab/Tactic/NormCast.lean

@@ -28,8 +28,10 @@ def proveEqUsing (s : SimpTheorems) (a b : Expr) : MetaM (Option Simp.Result) :=
     unless ← isDefEq a'.expr b'.expr do return none
     a'.mkEqTrans (← b'.mkEqSymm b)
   withReducible do
-    (go (← Simp.mkDefaultMethods).toMethodsRef
-      { simpTheorems := #[s], congrTheorems := ← Meta.getSimpCongrTheorems }).run' {}
+    let ctx ← Simp.mkContext
+        (simpTheorems := #[s])
+        (congrTheorems := ← Meta.getSimpCongrTheorems)
+    (go (← Simp.mkDefaultMethods).toMethodsRef ctx).run' {}
 
 /-- Proves `a = b` by simplifying using move and squash lemmas. -/
 def proveEqUsingDown (a b : Expr) : MetaM (Option Simp.Result) := do
@@ -191,19 +193,25 @@ def derive (e : Expr) : MetaM Simp.Result := do
   -- step 1: pre-processing of numerals
   let r ← withTrace "pre-processing numerals" do
     let post e := return Simp.Step.done (← try numeralToCoe e catch _ => pure {expr := e})
-    r.mkEqTrans (← Simp.main r.expr { config, congrTheorems } (methods := { post })).1
+    let ctx ← Simp.mkContext (config := config) (congrTheorems := congrTheorems)
+    r.mkEqTrans (← Simp.main r.expr ctx (methods := { post })).1
 
   -- step 2: casts are moved upwards and eliminated
   let r ← withTrace "moving upward, splitting and eliminating" do
     let post := upwardAndElim (← normCastExt.up.getTheorems)
-    r.mkEqTrans (← Simp.main r.expr { config, congrTheorems } (methods := { post })).1
+    let ctx ← Simp.mkContext (config := config) (congrTheorems := congrTheorems)
+    r.mkEqTrans (← Simp.main r.expr ctx (methods := { post })).1
 
   let simprocs ← ({} : Simp.SimprocsArray).add `reduceCtorEq false
 
   -- step 3: casts are squashed
   let r ← withTrace "squashing" do
     let simpTheorems := #[← normCastExt.squash.getTheorems]
-    r.mkEqTrans (← simp r.expr { simpTheorems, config, congrTheorems } simprocs).1
+    let ctx ← Simp.mkContext
+      (config := config)
+      (simpTheorems := simpTheorems)
+      (congrTheorems := congrTheorems)
+    r.mkEqTrans (← simp r.expr ctx simprocs).1
 
   return r
 
@@ -263,7 +271,7 @@ def evalConvNormCast : Tactic :=
 def evalPushCast : Tactic := fun stx => do
   let { ctx, simprocs, dischargeWrapper } ← withMainContext do
     mkSimpContext (simpTheorems := pushCastExt.getTheorems) stx (eraseLocal := false)
-  let ctx := { ctx with config := { ctx.config with failIfUnchanged := false } }
+  let ctx := ctx.setFailIfUnchanged false
   dischargeWrapper.with fun discharge? =>
     discard <| simpLocation ctx simprocs discharge? (expandOptLocation stx[5])
 

src/Lean/Elab/Tactic/Omega/Frontend.lean

@@ -6,7 +6,6 @@ Authors: Kim Morrison
 prelude
 import Lean.Elab.Tactic.Omega.Core
 import Lean.Elab.Tactic.FalseOrByContra
-import Lean.Meta.Tactic.Cases
 import Lean.Elab.Tactic.Config
 
 /-!
@@ -520,23 +519,6 @@ partial def processFacts (p : MetaProblem) : OmegaM (MetaProblem × Nat) := do
 
 end MetaProblem
 
-/--
-Given `p : P ∨ Q` (or any inductive type with two one-argument constructors),
-split the goal into two subgoals:
-one containing the hypothesis `h : P` and another containing `h : Q`.
--/
-def cases₂ (mvarId : MVarId) (p : Expr) (hName : Name := `h) :
-    MetaM ((MVarId × FVarId) × (MVarId × FVarId)) := do
-  let mvarId ← mvarId.assert `hByCases (← inferType p) p
-  let (fvarId, mvarId) ← mvarId.intro1
-  let #[s₁, s₂] ← mvarId.cases fvarId #[{ varNames := [hName] }, { varNames := [hName] }] |
-    throwError "'cases' tactic failed, unexpected number of subgoals"
-  let #[Expr.fvar f₁ ..] ← pure s₁.fields
-    | throwError "'cases' tactic failed, unexpected new hypothesis"
-  let #[Expr.fvar f₂ ..] ← pure s₂.fields
-    | throwError "'cases' tactic failed, unexpected new hypothesis"
-  return ((s₁.mvarId, f₁), (s₂.mvarId, f₂))
-
 /--
 Helpful error message when omega cannot find a solution
 -/
@@ -628,33 +610,36 @@ mutual
 Split a disjunction in a `MetaProblem`, and if we find a new usable fact
 call `omegaImpl` in both branches.
 -/
-partial def splitDisjunction (m : MetaProblem) (g : MVarId) : OmegaM Unit := g.withContext do
+partial def splitDisjunction (m : MetaProblem) : OmegaM Expr := do
   match m.disjunctions with
     | [] => throwError "omega could not prove the goal:\n{← formatErrorMessage m.problem}"
-    | h :: t =>
-      trace[omega] "Case splitting on {← inferType h}"
-      let ctx ← getMCtx
-      let (⟨g₁, h₁⟩, ⟨g₂, h₂⟩) ← cases₂ g h
-      trace[omega] "Adding facts:\n{← g₁.withContext <| inferType (.fvar h₁)}"
-      let m₁ := { m with facts := [.fvar h₁], disjunctions := t }
-      let r ← withoutModifyingState do
-        let (m₁, n) ← g₁.withContext m₁.processFacts
+    | h :: t => do
+      let hType ← whnfD (← inferType h)
+      trace[omega] "Case splitting on {hType}"
+      let_expr Or hType₁ hType₂ := hType | throwError "Unexpected disjunction {hType}"
+      let p?₁ ← withoutModifyingState do withLocalDeclD `h₁ hType₁ fun h₁ => do
+        withTraceNode `omega (msg := fun _ => do pure m!"Assuming fact:{indentExpr hType₁}") do
+        let m₁ := { m with facts := [h₁], disjunctions := t }
+        let (m₁, n) ← m₁.processFacts
         if 0 < n then
-          omegaImpl m₁ g₁
-          pure true
+          let p₁ ← omegaImpl m₁
+          let p₁ ← mkLambdaFVars #[h₁] p₁
+          return some p₁
         else
-          pure false
-      if r then
-        trace[omega] "Adding facts:\n{← g₂.withContext <| inferType (.fvar h₂)}"
-        let m₂ := { m with facts := [.fvar h₂], disjunctions := t }
-        omegaImpl m₂ g₂
+          return none
+      if let some p₁ := p?₁ then
+         withLocalDeclD `h₂ hType₂ fun h₂ => do
+          withTraceNode `omega (msg := fun _ => do pure m!"Assuming fact:{indentExpr hType₂}") do
+          let m₂ := { m with facts := [h₂], disjunctions := t }
+          let p₂ ← omegaImpl m₂
+          let p₂ ← mkLambdaFVars #[h₂] p₂
+          return mkApp6 (mkConst ``Or.elim) hType₁ hType₂ (mkConst ``False) h p₁ p₂
       else
         trace[omega] "No new facts found."
-        setMCtx ctx
-        splitDisjunction { m with disjunctions := t } g
+        splitDisjunction { m with disjunctions := t }
 
 /-- Implementation of the `omega` algorithm, and handling disjunctions. -/
-partial def omegaImpl (m : MetaProblem) (g : MVarId) : OmegaM Unit := g.withContext do
+partial def omegaImpl (m : MetaProblem) : OmegaM Expr := do
   let (m, _) ← m.processFacts
   guard m.facts.isEmpty
   let p := m.problem
@@ -663,12 +648,12 @@ partial def omegaImpl (m : MetaProblem) (g : MVarId) : OmegaM Unit := g.withCont
   trace[omega] "After elimination:\nAtoms: {← atomsList}\n{p'}"
   match p'.possible, p'.proveFalse?, p'.proveFalse?_spec with
   | true, _, _ =>
-    splitDisjunction m g
+    splitDisjunction m
   | false, .some prf, _ =>
     trace[omega] "Justification:\n{p'.explanation?.get}"
     let prf ← instantiateMVars (← prf)
     trace[omega] "omega found a contradiction, proving {← inferType prf}"
-    g.assign prf
+    return prf
 
 end
 
@@ -677,7 +662,9 @@ Given a collection of facts, try prove `False` using the omega algorithm,
 and close the goal using that.
 -/
 def omega (facts : List Expr) (g : MVarId) (cfg : OmegaConfig := {}) : MetaM Unit :=
-  OmegaM.run (omegaImpl { facts } g) cfg
+  g.withContext do
+    let prf ← OmegaM.run (omegaImpl { facts }) cfg
+    g.assign prf
 
 open Lean Elab Tactic Parser.Tactic
 

src/Lean/Elab/Tactic/Simp.lean

@@ -234,7 +234,7 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
             logException ex
           else
             throw ex
-      return { ctx := { ctx with simpTheorems := thmsArray.set! 0 thms }, simprocs, starArg }
+      return { ctx := ctx.setSimpTheorems (thmsArray.set! 0 thms), simprocs, starArg }
     -- If recovery is disabled, then we want simp argument elaboration failures to be exceptions.
     -- This affects `addSimpTheorem`.
     if (← read).recover then
@@ -311,10 +311,11 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp)
     simpTheorems
   let simprocs ← if simpOnly then pure {} else Simp.getSimprocs
   let congrTheorems ← getSimpCongrTheorems
-  let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) (simprocs := #[simprocs]) {
-    config      := (← elabSimpConfig stx[1] (kind := kind))
-    simpTheorems := #[simpTheorems], congrTheorems
-  }
+  let ctx ← Simp.mkContext
+     (config := (← elabSimpConfig stx[1] (kind := kind)))
+     (simpTheorems := #[simpTheorems])
+     congrTheorems
+  let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) (simprocs := #[simprocs]) ctx
   if !r.starArg || ignoreStarArg then
     return { r with dischargeWrapper }
   else
@@ -329,7 +330,7 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp)
     for h in hs do
       unless simpTheorems.isErased (.fvar h) do
         simpTheorems ← simpTheorems.addTheorem (.fvar h) (← h.getDecl).toExpr
-    let ctx := { ctx with simpTheorems }
+    let ctx := ctx.setSimpTheorems simpTheorems
     return { ctx, simprocs, dischargeWrapper }
 
 register_builtin_option tactic.simp.trace : Bool := {

src/Lean/Elab/Tactic/Simpa.lean

@@ -36,9 +36,9 @@ deriving instance Repr for UseImplicitLambdaResult
     let stx ← `(tactic| simp $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]?)
     let { ctx, simprocs, dischargeWrapper } ←
       withMainContext <| mkSimpContext stx (eraseLocal := false)
-    let ctx := if unfold.isSome then { ctx with config.autoUnfold := true } else ctx
+    let ctx := if unfold.isSome then ctx.setAutoUnfold else ctx
     -- TODO: have `simpa` fail if it doesn't use `simp`.
-    let ctx := { ctx with config := { ctx.config with failIfUnchanged := false } }
+    let ctx := ctx.setFailIfUnchanged false
     dischargeWrapper.with fun discharge? => do
       let (some (_, g), stats) ← simpGoal (← getMainGoal) ctx (simprocs := simprocs)
           (simplifyTarget := true) (discharge? := discharge?)

src/Lean/Message.lean

@@ -116,7 +116,7 @@ variable (p : Name → Bool) in
 /-- Returns true when the message contains a `MessageData.tagged tag ..` constructor where `p tag`
 is true.
 
-This does not descend into lazily generated subtress (`.ofLazy`); message tags
+This does not descend into lazily generated subtrees (`.ofLazy`); message tags
 of interest (like those added by `logLinter`) are expected to be near the root
 of the `MessageData`, and not hidden inside `.ofLazy`.
 -/
@@ -130,6 +130,19 @@ partial def hasTag : MessageData → Bool
   | trace data msg msgs     => p data.cls || hasTag msg || msgs.any hasTag
   | _                       => false
 
+/--
+Returns the top-level tag of the message.
+If none, returns `Name.anonymous`.
+
+This does not descend into message subtrees (e.g., `.compose`, `.ofLazy`).
+The message kind is expected to describe the whole message.
+-/
+def kind : MessageData → Name
+  | withContext _ msg       => kind msg
+  | withNamingContext _ msg => kind msg
+  | tagged n _              => n
+  | _                       => .anonymous
+
 /-- An empty message. -/
 def nil : MessageData :=
   ofFormat Format.nil
@@ -315,7 +328,7 @@ structure BaseMessage (α : Type u) where
   endPos        : Option Position := none
   /-- If `true`, report range as given; see `msgToInteractiveDiagnostic`. -/
   keepFullRange : Bool := false
-  severity      : MessageSeverity := MessageSeverity.error
+  severity      : MessageSeverity := .error
   caption       : String          := ""
   /-- The content of the message. -/
   data          : α
@@ -328,7 +341,10 @@ abbrev Message := BaseMessage MessageData
 /-- A `SerialMessage` is a `Message` whose `MessageData` has been eagerly
 serialized and is thus appropriate for use in pure contexts where the effectful
 `MessageData.toString` cannot be used. -/
-abbrev SerialMessage := BaseMessage String
+structure SerialMessage extends BaseMessage String where
+  /-- The message kind (i.e., the top-level tag). -/
+  kind          : Name
+  deriving ToJson, FromJson
 
 namespace SerialMessage
 
@@ -354,8 +370,12 @@ end SerialMessage
 
 namespace Message
 
+@[inherit_doc MessageData.kind] abbrev kind (msg : Message) :=
+  msg.data.kind
+
+/-- Serializes the message, converting its data into a string and saving its kind. -/
 @[inline] def serialize (msg : Message) : IO SerialMessage := do
-  return {msg with data := ← msg.data.toString}
+  return {msg with kind := msg.kind, data := ← msg.data.toString}
 
 protected def toString (msg : Message) (includeEndPos := false) : IO String := do
   -- Remark: The inline here avoids a new message allocation when `msg` is shared

src/Lean/Meta/Basic.lean

@@ -332,7 +332,7 @@ register_builtin_option maxSynthPendingDepth : Nat := {
   Contextual information for the `MetaM` monad.
 -/
 structure Context where
-  config            : Config               := {}
+  private config    : Config               := {}
   /-- Local context -/
   lctx              : LocalContext         := {}
   /-- Local instances in `lctx`. -/
@@ -943,6 +943,15 @@ def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool := false) :
 @[inline] def withConfig (f : Config → Config) : n α → n α :=
   mapMetaM <| withReader (fun ctx => { ctx with config := f ctx.config })
 
+@[inline] def withCanUnfoldPred (p : Config → ConstantInfo → CoreM Bool) : n α → n α :=
+  mapMetaM <| withReader (fun ctx => { ctx with canUnfold? := p })
+
+@[inline] def withIncSynthPending : n α → n α :=
+  mapMetaM <| withReader (fun ctx => { ctx with synthPendingDepth := ctx.synthPendingDepth + 1 })
+
+@[inline] def withInTypeClassResolution : n α → n α :=
+  mapMetaM <| withReader (fun ctx => { ctx with inTypeClassResolution := true })
+
 /--
 Executes `x` tracking zetaDelta reductions `Config.trackZetaDelta := true`
 -/
@@ -1422,6 +1431,14 @@ def withLocalDecl (name : Name) (bi : BinderInfo) (type : Expr) (k : Expr → n
 def withLocalDeclD (name : Name) (type : Expr) (k : Expr → n α) : n α :=
   withLocalDecl name BinderInfo.default type k
 
+/--
+Similar to `withLocalDecl`, but it does **not** check whether the new variable is a local instance or not.
+-/
+def withLocalDeclNoLocalInstanceUpdate (name : Name) (bi : BinderInfo) (type : Expr) (x : Expr → MetaM α) : MetaM α := do
+  let fvarId ← mkFreshFVarId
+  withReader (fun ctx => { ctx with lctx := ctx.lctx.mkLocalDecl fvarId name type bi }) do
+    x (mkFVar fvarId)
+
 /-- Append an array of free variables `xs` to the local context and execute `k xs`.
 `declInfos` takes the form of an array consisting of:
 - the name of the variable
@@ -1538,11 +1555,11 @@ def withReplaceFVarId {α} (fvarId : FVarId) (e : Expr) : MetaM α → MetaM α
     localInstances := ctx.localInstances.erase fvarId }
 
 /--
-  `withNewMCtxDepth k` executes `k` with a higher metavariable context depth,
-  where metavariables created outside the `withNewMCtxDepth` (with a lower depth) cannot be assigned.
-  If `allowLevelAssignments` is set to true, then the level metavariable depth
-  is not increased, and level metavariables from the outer scope can be
-  assigned.  (This is used by TC synthesis.)
+`withNewMCtxDepth k` executes `k` with a higher metavariable context depth,
+where metavariables created outside the `withNewMCtxDepth` (with a lower depth) cannot be assigned.
+If `allowLevelAssignments` is set to true, then the level metavariable depth
+is not increased, and level metavariables from the outer scope can be
+assigned.  (This is used by TC synthesis.)
 -/
 def withNewMCtxDepth (k : n α) (allowLevelAssignments := false) : n α :=
   mapMetaM (withNewMCtxDepthImp allowLevelAssignments) k
@@ -1552,13 +1569,20 @@ private def withLocalContextImp (lctx : LocalContext) (localInsts : LocalInstanc
     x
 
 /--
-  `withLCtx lctx localInsts k` replaces the local context and local instances, and then executes `k`.
-  The local context and instances are restored after executing `k`.
-  This method assumes that the local instances in `localInsts` are in the local context `lctx`.
+`withLCtx lctx localInsts k` replaces the local context and local instances, and then executes `k`.
+The local context and instances are restored after executing `k`.
+This method assumes that the local instances in `localInsts` are in the local context `lctx`.
 -/
 def withLCtx (lctx : LocalContext) (localInsts : LocalInstances) : n α → n α :=
   mapMetaM <| withLocalContextImp lctx localInsts
 
+/--
+Simpler version of `withLCtx` which just updates the local context. It is the resposability of the
+caller ensure the local instances are also properly updated.
+-/
+def withLCtx' (lctx : LocalContext) : n α → n α :=
+  mapMetaM <| withReader (fun ctx => { ctx with lctx })
+
 /--
 Runs `k` in a local environment with the `fvarIds` erased.
 -/

src/Lean/Meta/Coe.lean

@@ -157,9 +157,11 @@ def coerceMonadLift? (e expectedType : Expr) : MetaM (Option Expr) := do
   let eType ← instantiateMVars (← inferType e)
   let some (n, β) ← isTypeApp? expectedType | return none
   let some (m, α) ← isTypeApp? eType | return none
+  -- Need to save and restore the state in case `m` and `n` are defeq but not monads to prevent this procedure from having side effects.
+  let saved ← saveState
   if (← isDefEq m n) then
-    let some monadInst ← isMonad? n | return none
-    try expandCoe (← mkAppOptM ``Lean.Internal.coeM #[m, α, β, none, monadInst, e]) catch _ => return none
+    let some monadInst ← isMonad? n | restoreState saved; return none
+    try expandCoe (← mkAppOptM ``Lean.Internal.coeM #[m, α, β, none, monadInst, e]) catch _ => restoreState saved; return none
   else if autoLift.get (← getOptions) then
     try
       -- Construct lift from `m` to `n`

src/Lean/Meta/DiscrTree.lean

@@ -553,8 +553,8 @@ private def getKeyArgs (e : Expr) (isMatch root : Bool) (config : WhnfCoreConfig
     if isMatch then
       return (.other, #[])
     else do
-      let ctx ← read
-      if ctx.config.isDefEqStuckEx then
+      let cfg ← getConfig
+      if cfg.isDefEqStuckEx then
         /-
           When the configuration flag `isDefEqStuckEx` is set to true,
           we want `isDefEq` to throw an exception whenever it tries to assign

src/Lean/Meta/ExprDefEq.lean

@@ -364,7 +364,7 @@ private partial def isDefEqBindingAux (lctx : LocalContext) (fvars : Array Expr)
   | Expr.forallE n d₁ b₁ _, Expr.forallE _ d₂ b₂ _ => process n d₁ d₂ b₁ b₂
   | Expr.lam     n d₁ b₁ _, Expr.lam     _ d₂ b₂ _ => process n d₁ d₂ b₁ b₂
   | _,                      _                      =>
-    withReader (fun ctx => { ctx with lctx := lctx }) do
+    withLCtx' lctx do
       isDefEqBindingDomain fvars ds₂ do
         Meta.isExprDefEqAux (e₁.instantiateRev fvars) (e₂.instantiateRev fvars)
 
@@ -758,8 +758,8 @@ mutual
     if mvarDecl.depth != (← getMCtx).depth || mvarDecl.kind.isSyntheticOpaque then
       traceM `Meta.isDefEq.assign.readOnlyMVarWithBiggerLCtx <| addAssignmentInfo (mkMVar mvarId)
       throwCheckAssignmentFailure
-    let ctxMeta ← readThe Meta.Context
-    unless ctxMeta.config.ctxApprox && ctx.mvarDecl.lctx.isSubPrefixOf mvarDecl.lctx do
+    let cfg ← getConfig
+    unless cfg.ctxApprox && ctx.mvarDecl.lctx.isSubPrefixOf mvarDecl.lctx do
       traceM `Meta.isDefEq.assign.readOnlyMVarWithBiggerLCtx <| addAssignmentInfo (mkMVar mvarId)
       throwCheckAssignmentFailure
     /- Create an auxiliary metavariable with a smaller context and "checked" type.
@@ -814,8 +814,8 @@ mutual
 
   partial def checkApp (e : Expr) : CheckAssignmentM Expr :=
     e.withApp fun f args => do
-      let ctxMeta ← readThe Meta.Context
-      if f.isMVar && ctxMeta.config.ctxApprox && args.all Expr.isFVar then
+      let cfg ← getConfig
+      if f.isMVar && cfg.ctxApprox && args.all Expr.isFVar then
         let f ← check f
         catchInternalId outOfScopeExceptionId
           (do
@@ -1794,8 +1794,8 @@ private partial def isDefEqQuickOther (t s : Expr) : MetaM LBool := do
         | LBool.true => return LBool.true
         | LBool.false => return LBool.false
         | _ =>
-          let ctx ← read
-          if ctx.config.isDefEqStuckEx then do
+          let cfg ← getConfig
+          if cfg.isDefEqStuckEx then do
             trace[Meta.isDefEq.stuck] "{t} =?= {s}"
             Meta.throwIsDefEqStuck
           else
@@ -1834,7 +1834,7 @@ end
       let e ← instantiateMVars e
       successK e
     else
-      if (← read).config.isDefEqStuckEx then
+      if (← getConfig).isDefEqStuckEx then
         /-
         When `isDefEqStuckEx := true` and `mvar` was created in a previous level,
         we should throw an exception. See issue #2736 for a situation where this can happen.

src/Lean/Meta/GetUnfoldableConst.lean

@@ -22,10 +22,11 @@ private def canUnfoldDefault (cfg : Config) (info : ConstantInfo) : CoreM Bool :
 
 def canUnfold (info : ConstantInfo) : MetaM Bool := do
   let ctx ← read
+  let cfg ← getConfig
   if let some f := ctx.canUnfold? then
-    f ctx.config info
+    f cfg info
   else
-    canUnfoldDefault ctx.config info
+    canUnfoldDefault cfg info
 
 /--
 Look up a constant name, returning the `ConstantInfo`

src/Lean/Meta/InferType.lean

@@ -382,11 +382,6 @@ def isType (e : Expr) : MetaM Bool := do
     | .sort .. => return true
     | _        => return false
 
-@[inline] private def withLocalDecl' {α} (name : Name) (bi : BinderInfo) (type : Expr) (x : Expr → MetaM α) : MetaM α := do
-  let fvarId ← mkFreshFVarId
-  withReader (fun ctx => { ctx with lctx := ctx.lctx.mkLocalDecl fvarId name type bi }) do
-    x (mkFVar fvarId)
-
 def typeFormerTypeLevelQuick : Expr → Option Level
   | .forallE _ _ b _ => typeFormerTypeLevelQuick b
   | .sort l => some l
@@ -403,7 +398,7 @@ where
   go (type : Expr) (xs : Array Expr) : MetaM (Option Level) := do
     match type with
     | .sort l => return some l
-    | .forallE n d b c => withLocalDecl' n c (d.instantiateRev xs) fun x => go b (xs.push x)
+    | .forallE n d b c => withLocalDeclNoLocalInstanceUpdate n c (d.instantiateRev xs) fun x => go b (xs.push x)
     | _ =>
       let type ← whnfD (type.instantiateRev xs)
       match type with

src/Lean/Meta/LazyDiscrTree.lean

@@ -222,8 +222,8 @@ private def getKeyArgs (e : Expr) (isMatch root : Bool) (config : WhnfCoreConfig
     if isMatch then
       return (.other, #[])
     else do
-      let ctx ← read
-      if ctx.config.isDefEqStuckEx then
+      let cfg ← getConfig
+      if cfg.isDefEqStuckEx then
         /-
           When the configuration flag `isDefEqStuckEx` is set to true,
           we want `isDefEq` to throw an exception whenever it tries to assign

src/Lean/Meta/LevelDefEq.lean

@@ -149,8 +149,8 @@ mutual
             if r != LBool.undef then
               return r == LBool.true
             else if !(← hasAssignableLevelMVar lhs <||> hasAssignableLevelMVar rhs) then
-              let ctx ← read
-              if ctx.config.isDefEqStuckEx && (lhs.isMVar || rhs.isMVar) then do
+              let cfg ← getConfig
+              if cfg.isDefEqStuckEx && (lhs.isMVar || rhs.isMVar) then do
                 trace[Meta.isLevelDefEq.stuck] "{lhs} =?= {rhs}"
                 Meta.throwIsDefEqStuck
               else

src/Lean/Meta/Match/MatcherApp/Transform.lean

@@ -162,7 +162,7 @@ def refineThrough? (matcherApp : MatcherApp) (e : Expr) :
 private def withUserNamesImpl {α} (fvars : Array Expr) (names : Array Name) (k : MetaM α) : MetaM α := do
   let lctx := (Array.zip fvars names).foldl (init := ← (getLCtx)) fun lctx (fvar, name) =>
     lctx.setUserName fvar.fvarId! name
-  withTheReader Meta.Context (fun ctx => { ctx with lctx }) k
+  withLCtx' lctx k
 
 /--
 Sets the user name of the FVars in the local context according to the given array of names.

src/Lean/Meta/SynthInstance.lean

@@ -782,7 +782,7 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
     (return m!"{exceptOptionEmoji ·} {← instantiateMVars type}") do
   withConfig (fun config => { config with isDefEqStuckEx := true, transparency := TransparencyMode.instances,
                                           foApprox := true, ctxApprox := true, constApprox := false, univApprox := false }) do
-  withReader (fun ctx => { ctx with inTypeClassResolution := true }) do
+  withInTypeClassResolution do
     let localInsts ← getLocalInstances
     let type ← instantiateMVars type
     let type ← preprocess type
@@ -839,7 +839,7 @@ private def synthPendingImp (mvarId : MVarId) : MetaM Bool := withIncRecDepth <|
         recordSynthPendingFailure mvarDecl.type
         return false
       else
-        withReader (fun ctx => { ctx with synthPendingDepth := ctx.synthPendingDepth + 1 }) do
+        withIncSynthPending do
           trace[Meta.synthPending] "synthPending {mkMVar mvarId}"
           let val? ← catchInternalId isDefEqStuckExceptionId (synthInstance? mvarDecl.type (maxResultSize? := none)) (fun _ => pure none)
           match val? with

src/Lean/Meta/Tactic/AC/Main.lean

@@ -188,12 +188,10 @@ def post (e : Expr) : SimpM Simp.Step := do
   | e, _ => return Simp.Step.done { expr := e }
 
 def rewriteUnnormalized (mvarId : MVarId) : MetaM MVarId := do
-  let simpCtx :=
-    {
-      simpTheorems  := {}
-      congrTheorems := (← getSimpCongrTheorems)
-      config        := Simp.neutralConfig
-    }
+  let simpCtx ← Simp.mkContext
+      (simpTheorems  := {})
+      (congrTheorems := (← getSimpCongrTheorems))
+      (config        := Simp.neutralConfig)
   let tgt ← instantiateMVars (← mvarId.getType)
   let (res, _) ← Simp.main tgt simpCtx (methods := { post })
   applySimpResultToTarget mvarId tgt res
@@ -207,12 +205,10 @@ def rewriteUnnormalizedRefl (goal : MVarId) : MetaM Unit := do
 
 def acNfHypMeta (goal : MVarId) (fvarId : FVarId) : MetaM (Option MVarId) := do
   goal.withContext do
-    let simpCtx :=
-    {
-      simpTheorems  := {}
-      congrTheorems := (← getSimpCongrTheorems)
-      config        := Simp.neutralConfig
-    }
+    let simpCtx ← Simp.mkContext
+      (simpTheorems  := {})
+      (congrTheorems := (← getSimpCongrTheorems))
+      (config        := Simp.neutralConfig)
     let tgt ← instantiateMVars (← fvarId.getType)
     let (res, _) ← Simp.main tgt simpCtx (methods := { post })
     return (← applySimpResultToLocalDecl goal fvarId res false).map (·.snd)

src/Lean/Meta/Tactic/Acyclic.lean

@@ -38,7 +38,10 @@ where
       let sizeOfEq ← mkLT sizeOf_lhs sizeOf_rhs
       let hlt ← mkFreshExprSyntheticOpaqueMVar sizeOfEq
       -- TODO: we only need the `sizeOf` simp theorems
-      match (← simpTarget hlt.mvarId! { config.arith := true, simpTheorems := #[ (← getSimpTheorems) ] } {}).1 with
+      let ctx ← Simp.mkContext
+         (config := { arith := true })
+         (simpTheorems := #[ (← getSimpTheorems) ])
+      match (← simpTarget hlt.mvarId! ctx {}).1 with
       | some _ => return false
       | none   =>
         let heq ← mkCongrArg sizeOf_lhs.appFn! (← mkEqSymm h)

src/Lean/Meta/Tactic/Apply.lean

@@ -254,10 +254,6 @@ Apply `And.intro` as much as possible to goal `mvarId`.
 abbrev splitAnd (mvarId : MVarId) : MetaM (List MVarId) :=
   splitAndCore mvarId
 
-@[deprecated splitAnd (since := "2024-03-17")]
-def _root_.Lean.Meta.splitAnd (mvarId : MVarId) : MetaM (List MVarId) :=
-  mvarId.splitAnd
-
 def exfalso (mvarId : MVarId) : MetaM MVarId :=
   mvarId.withContext do
     mvarId.checkNotAssigned `exfalso

src/Lean/Meta/Tactic/Grind/Preprocessor.lean

@@ -38,11 +38,10 @@ abbrev PreM := ReaderT Context $ StateRefT State GrindM
 def PreM.run (x : PreM α) : GrindM α := do
   let thms ← grindNormExt.getTheorems
   let simprocs := #[(← grindNormSimprocExt.getSimprocs)]
-  let simp : Simp.Context := {
-    config := { arith := true }
-    simpTheorems := #[thms]
-    congrTheorems := (← getSimpCongrTheorems)
-  }
+  let simp ← Simp.mkContext
+    (config := { arith := true })
+    (simpTheorems := #[thms])
+    (congrTheorems := (← getSimpCongrTheorems))
   x { simp, simprocs } |>.run' {}
 
 def simp (_goal : Goal) (e : Expr) : PreM Simp.Result := do

src/Lean/Meta/Tactic/Intro.lean

@@ -17,7 +17,7 @@ namespace Lean.Meta
     match i, type with
     | 0, type =>
       let type := type.instantiateRevRange j fvars.size fvars
-      withReader (fun ctx => { ctx with lctx := lctx }) do
+      withLCtx' lctx do
         withNewLocalInstances fvars j do
           let tag     ← mvarId.getTag
           let type := type.headBeta
@@ -57,7 +57,7 @@ namespace Lean.Meta
         loop i lctx fvars j s body
       else
         let type := type.instantiateRevRange j fvars.size fvars
-        withReader (fun ctx => { ctx with lctx := lctx }) do
+        withLCtx' lctx do
           withNewLocalInstances fvars j do
             /- We used to use just `whnf`, but it produces counterintuitive behavior if
               - `type` is a metavariable `?m` such that `?m := let x := v; b`, or

src/Lean/Meta/Tactic/LinearArith/Nat/Basic.lean

@@ -8,6 +8,7 @@ import Lean.Meta.Check
 import Lean.Meta.Offset
 import Lean.Meta.AppBuilder
 import Lean.Meta.KExprMap
+import Lean.Data.RArray
 
 namespace Lean.Meta.Linear.Nat
 
@@ -141,8 +142,11 @@ end ToLinear
 
 export ToLinear (toLinearCnstr? toLinearExpr)
 
-def toContextExpr (ctx : Array Expr) : MetaM Expr := do
-  mkListLit (mkConst ``Nat) ctx.toList
+def toContextExpr (ctx : Array Expr) : Expr :=
+  if h : 0 < ctx.size then
+    RArray.toExpr (mkConst ``Nat) id (RArray.ofArray ctx h)
+  else
+    RArray.toExpr (mkConst ``Nat) id (RArray.leaf (mkNatLit 0))
 
 def reflTrue : Expr :=
   mkApp2 (mkConst ``Eq.refl [levelOne]) (mkConst ``Bool) (mkConst ``Bool.true)

src/Lean/Meta/Tactic/LinearArith/Nat/Simp.lean

@@ -31,17 +31,17 @@ def simpCnstrPos? (e : Expr) : MetaM (Option (Expr × Expr)) := do
     let c₂ := c₁.norm
     if c₂.isUnsat then
       let r := mkConst ``False
-      let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_false_of_isUnsat) (← toContextExpr ctx) (toExpr c) reflTrue
+      let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_false_of_isUnsat) (toContextExpr ctx) (toExpr c) reflTrue
       return some (r, ← mkExpectedTypeHint p (← mkEq lhs r))
     else if c₂.isValid then
       let r := mkConst ``True
-      let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_true_of_isValid) (← toContextExpr ctx) (toExpr c) reflTrue
+      let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_true_of_isValid) (toContextExpr ctx) (toExpr c) reflTrue
       return some (r, ← mkExpectedTypeHint p (← mkEq lhs r))
     else
       let c₂ : LinearCnstr := c₂.toExpr
       let r ← c₂.toArith ctx
       if r != lhs then
-        let p := mkApp4 (mkConst ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq) (← toContextExpr ctx) (toExpr c) (toExpr c₂) reflTrue
+        let p := mkApp4 (mkConst ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq) (toContextExpr ctx) (toExpr c) (toExpr c₂) reflTrue
         return some (r, ← mkExpectedTypeHint p (← mkEq lhs r))
       else
         return none
@@ -81,7 +81,7 @@ def simpExpr? (e : Expr) : MetaM (Option (Expr × Expr)) := do
   if p'.length < p.length then
     -- We only return some if monomials were fused
     let e' : LinearExpr := p'.toExpr
-    let p := mkApp4 (mkConst ``Nat.Linear.Expr.eq_of_toNormPoly_eq) (← toContextExpr ctx) (toExpr e) (toExpr e') reflTrue
+    let p := mkApp4 (mkConst ``Nat.Linear.Expr.eq_of_toNormPoly_eq) (toContextExpr ctx) (toExpr e) (toExpr e') reflTrue
     let r ← e'.toArith ctx
     return some (r, p)
   else

src/Lean/Meta/Tactic/LinearArith/Solver.lean

@@ -6,9 +6,10 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Ord
 import Init.Data.Array.DecidableEq
-import Lean.Data.Rat
+import Std.Internal.Rat
 
 namespace Lean.Meta.Linear
+open Std.Internal
 
 structure Var where
   id : Nat

src/Lean/Meta/Tactic/Rewrites.lean

@@ -60,9 +60,6 @@ private def addImport (name : Name) (constInfo : ConstantInfo) :
         pure a
       | _ => return #[]
 
-/-- Configuration for `DiscrTree`. -/
-def discrTreeConfig : WhnfCoreConfig := {}
-
 /-- Select `=` and `↔` local hypotheses. -/
 def localHypotheses (except : List FVarId := []) : MetaM (Array (Expr × Bool × Nat)) := do
   let r ← getLocalHyps

src/Lean/Meta/Tactic/Simp/Attr.lean

@@ -73,7 +73,10 @@ def getSimpTheorems : CoreM SimpTheorems :=
 def getSEvalTheorems : CoreM SimpTheorems :=
   sevalSimpExtension.getTheorems
 
-def Simp.Context.mkDefault : MetaM Context :=
-  return { config := {}, simpTheorems := #[(← Meta.getSimpTheorems)], congrTheorems := (← Meta.getSimpCongrTheorems) }
+def Simp.Context.mkDefault : MetaM Context := do
+  mkContext
+    (config := {})
+    (simpTheorems := #[(← Meta.getSimpTheorems)])
+    (congrTheorems := (← Meta.getSimpCongrTheorems))
 
 end Lean.Meta

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -20,18 +20,6 @@ builtin_initialize congrHypothesisExceptionId : InternalExceptionId ←
 def throwCongrHypothesisFailed : MetaM α :=
   throw <| Exception.internal congrHypothesisExceptionId
 
-/--
-  Helper method for bootstrapping purposes. It disables `arith` if support theorems have not been defined yet.
--/
-def Config.updateArith (c : Config) : CoreM Config := do
-  if c.arith then
-    if (← getEnv).contains ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq then
-      return c
-    else
-      return { c with arith := false }
-  else
-    return c
-
 /-- Return true if `e` is of the form `ofNat n` where `n` is a kernel Nat literal -/
 def isOfNatNatLit (e : Expr) : Bool :=
   e.isAppOf ``OfNat.ofNat && e.getAppNumArgs >= 3 && (e.getArg! 1).isRawNatLit
@@ -256,7 +244,7 @@ def withNewLemmas {α} (xs : Array Expr) (f : SimpM α) : SimpM α := do
           s ← s.addTheorem (.fvar x.fvarId!) x
           updated := true
       if updated then
-        withTheReader Context (fun ctx => { ctx with simpTheorems := s }) f
+        withSimpTheorems s f
       else
         f
   else if (← getMethods).wellBehavedDischarge then
@@ -463,7 +451,7 @@ private partial def dsimpImpl (e : Expr) : SimpM Expr := do
   let m ← getMethods
   let pre := m.dpre >> doNotVisitOfNat >> doNotVisitOfScientific >> doNotVisitCharLit
   let post := m.dpost >> dsimpReduce
-  withTheReader Simp.Context (fun ctx => { ctx with inDSimp := true }) do
+  withInDSimp do
   transform (usedLetOnly := cfg.zeta) e (pre := pre) (post := post)
 
 def visitFn (e : Expr) : SimpM Result := do
@@ -658,11 +646,12 @@ where
     trace[Meta.Tactic.simp.heads] "{repr e.toHeadIndex}"
     simpLoop e
 
+-- TODO: delete
 @[inline] def withSimpContext (ctx : Context) (x : MetaM α) : MetaM α :=
   withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| withReducible x
 
 def main (e : Expr) (ctx : Context) (stats : Stats := {}) (methods : Methods := {}) : MetaM (Result × Stats) := do
-  let ctx := { ctx with config := (← ctx.config.updateArith), lctxInitIndices := (← getLCtx).numIndices }
+  let ctx ← ctx.setLctxInitIndices
   withSimpContext ctx do
     let (r, s) ← go e methods.toMethodsRef ctx |>.run { stats with }
     trace[Meta.Tactic.simp.numSteps] "{s.numSteps}"
@@ -810,7 +799,7 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsArray :=
     for fvarId in fvarIdsToSimp do
       let localDecl ← fvarId.getDecl
       let type ← instantiateMVars localDecl.type
-      let ctx := { ctx with simpTheorems := ctx.simpTheorems.eraseTheorem (.fvar localDecl.fvarId) }
+      let ctx := ctx.setSimpTheorems <| ctx.simpTheorems.eraseTheorem (.fvar localDecl.fvarId)
       let (r, stats') ← simp type ctx simprocs discharge? stats
       stats := stats'
       match r.proof? with
@@ -844,7 +833,7 @@ def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsAr
     let localDecl ← h.getDecl
     let proof  := localDecl.toExpr
     let simpTheorems ← ctx.simpTheorems.addTheorem (.fvar h) proof
-    ctx := { ctx with simpTheorems }
+    ctx := ctx.setSimpTheorems simpTheorems
   match (← simpTarget mvarId ctx simprocs discharge? (stats := stats)) with
   | (none, stats) => return (TacticResultCNM.closed, stats)
   | (some mvarId', stats') =>

src/Lean/Meta/Tactic/Simp/Rewrite.lean

@@ -41,7 +41,7 @@ def discharge?' (thmId : Origin) (x : Expr) (type : Expr) : SimpM Bool := do
     let ctx ← getContext
     if ctx.dischargeDepth >= ctx.maxDischargeDepth then
       return .maxDepth
-    else withTheReader Context (fun ctx => { ctx with dischargeDepth := ctx.dischargeDepth + 1 }) do
+    else withIncDischargeDepth do
       -- We save the state, so that `UsedTheorems` does not accumulate
       -- `simp` lemmas used during unsuccessful discharging.
       -- We use `withPreservedCache` to ensure the cache is restored after `discharge?`
@@ -446,10 +446,13 @@ def mkSEvalMethods : CoreM Methods := do
     wellBehavedDischarge := true
   }
 
-def mkSEvalContext : CoreM Context := do
+def mkSEvalContext : MetaM Context := do
   let s ← getSEvalTheorems
   let c ← Meta.getSimpCongrTheorems
-  return { simpTheorems := #[s], congrTheorems := c, config := { ground := true } }
+  mkContext
+    (simpTheorems := #[s])
+    (congrTheorems := c)
+    (config := { ground := true })
 
 /--
 Invoke ground/symbolic evaluator from `simp`.
@@ -552,7 +555,7 @@ private def dischargeUsingAssumption? (e : Expr) : SimpM (Option Expr) := do
 partial def dischargeEqnThmHypothesis? (e : Expr) : MetaM (Option Expr) := do
   assert! isEqnThmHypothesis e
   let mvar ← mkFreshExprSyntheticOpaqueMVar e
-  withReader (fun ctx => { ctx with canUnfold? := canUnfoldAtMatcher }) do
+  withCanUnfoldPred canUnfoldAtMatcher do
     if let .none ← go? mvar.mvarId! then
       instantiateMVars mvar
     else

src/Lean/Meta/Tactic/Simp/SimpAll.lean

@@ -43,7 +43,7 @@ private def initEntries : M Unit := do
       let localDecl ← h.getDecl
       let proof  := localDecl.toExpr
       simpThms ← simpThms.addTheorem (.fvar h) proof
-      modify fun s => { s with ctx.simpTheorems := simpThms }
+      modify fun s => { s with ctx := s.ctx.setSimpTheorems simpThms }
       if hsNonDeps.contains h then
         -- We only simplify nondependent hypotheses
         let type ← instantiateMVars localDecl.type
@@ -62,7 +62,7 @@ private partial def loop : M Bool := do
     let ctx := (← get).ctx
     -- We disable the current entry to prevent it to be simplified to `True`
     let simpThmsWithoutEntry := (← getSimpTheorems).eraseTheorem entry.id
-    let ctx := { ctx with simpTheorems := simpThmsWithoutEntry }
+    let ctx := ctx.setSimpTheorems simpThmsWithoutEntry
     let (r, stats) ← simpStep (← get).mvarId entry.proof entry.type ctx simprocs (stats := { (← get) with })
     modify fun s => { s with usedTheorems := stats.usedTheorems, diag := stats.diag }
     match r with
@@ -98,7 +98,7 @@ private partial def loop : M Bool := do
         simpThmsNew ← simpThmsNew.addTheorem (.other idNew) (← mkExpectedTypeHint proofNew typeNew)
         modify fun s => { s with
           modified         := true
-          ctx.simpTheorems := simpThmsNew
+          ctx              := ctx.setSimpTheorems simpThmsNew
           entries[i]       := { entry with type := typeNew, proof := proofNew, id := .other idNew }
         }
   -- simplify target

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -52,6 +52,7 @@ abbrev Cache := SExprMap Result
 abbrev CongrCache := ExprMap (Option CongrTheorem)
 
 structure Context where
+  private mk ::
   config           : Config := {}
   /-- `maxDischargeDepth` from `config` as an `UInt32`. -/
   maxDischargeDepth : UInt32 := UInt32.ofNatTruncate config.maxDischargeDepth
@@ -103,6 +104,41 @@ structure Context where
   inDSimp : Bool := false
   deriving Inhabited
 
+/--
+Helper method for bootstrapping purposes.
+It disables `arith` if support theorems have not been defined yet.
+-/
+private def updateArith (c : Config) : CoreM Config := do
+  if c.arith then
+    if (← getEnv).contains ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq then
+      return c
+    else
+      return { c with arith := false }
+  else
+    return c
+
+def mkContext (config : Config := {}) (simpTheorems : SimpTheoremsArray := {}) (congrTheorems : SimpCongrTheorems := {}) : MetaM Context := do
+  let config ← updateArith config
+  return { config, simpTheorems, congrTheorems }
+
+def Context.setConfig (context : Context) (config : Config) : Context :=
+  { context with config }
+
+def Context.setSimpTheorems (c : Context) (simpTheorems : SimpTheoremsArray) : Context :=
+  { c with simpTheorems }
+
+def Context.setLctxInitIndices (c : Context) : MetaM Context :=
+  return { c with lctxInitIndices := (← getLCtx).numIndices }
+
+def Context.setAutoUnfold (c : Context) : Context :=
+  { c with config.autoUnfold := true }
+
+def Context.setFailIfUnchanged (c : Context) (flag : Bool) : Context :=
+  { c with config.failIfUnchanged := flag }
+
+def Context.setMemoize (c : Context) (flag : Bool) : Context :=
+  { c with config.memoize := flag }
+
 def Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool :=
   ctx.simpTheorems.isDeclToUnfold declName
 
@@ -158,6 +194,15 @@ instance : Nonempty MethodsRef := MethodsRefPointed.property
 
 abbrev SimpM := ReaderT MethodsRef $ ReaderT Context $ StateRefT State MetaM
 
+@[inline] def withIncDischargeDepth : SimpM α → SimpM α :=
+  withTheReader Context (fun ctx => { ctx with dischargeDepth := ctx.dischargeDepth + 1 })
+
+@[inline] def withSimpTheorems (s : SimpTheoremsArray) : SimpM α → SimpM α :=
+  withTheReader Context (fun ctx => { ctx with simpTheorems := s })
+
+@[inline] def withInDSimp : SimpM α → SimpM α :=
+  withTheReader Context (fun ctx => { ctx with inDSimp := true })
+
 @[extern "lean_simp"]
 opaque simp (e : Expr) : SimpM Result
 

src/Lean/Meta/Tactic/Split.lean

@@ -13,12 +13,11 @@ import Lean.Meta.Tactic.Generalize
 namespace Lean.Meta
 namespace Split
 
-def getSimpMatchContext : MetaM Simp.Context :=
-   return {
-      simpTheorems   := {}
-      congrTheorems := (← getSimpCongrTheorems)
-      config        := { Simp.neutralConfig with dsimp := false }
-   }
+def getSimpMatchContext : MetaM Simp.Context := do
+   Simp.mkContext
+      (simpTheorems   := {})
+      (congrTheorems := (← getSimpCongrTheorems))
+      (config        := { Simp.neutralConfig with dsimp := false })
 
 def simpMatch (e : Expr) : MetaM Simp.Result := do
   let discharge? ← SplitIf.mkDischarge?

src/Lean/Meta/Tactic/SplitIf.lean

@@ -19,11 +19,10 @@ def getSimpContext : MetaM Simp.Context := do
   s ← s.addConst ``if_neg
   s ← s.addConst ``dif_pos
   s ← s.addConst ``dif_neg
-  return {
-    simpTheorems  := #[s]
-    congrTheorems := (← getSimpCongrTheorems)
-    config        := { Simp.neutralConfig with dsimp := false }
-  }
+  Simp.mkContext
+    (simpTheorems  := #[s])
+    (congrTheorems := (← getSimpCongrTheorems))
+    (config        := { Simp.neutralConfig with dsimp := false })
 
 /--
   Default `discharge?` function for `simpIf` methods.

src/Lean/Meta/Tactic/Unfold.lean

@@ -10,11 +10,10 @@ import Lean.Meta.Tactic.Simp.Main
 
 namespace Lean.Meta
 
-private def getSimpUnfoldContext : MetaM Simp.Context :=
-   return {
-      congrTheorems := (← getSimpCongrTheorems)
-      config        := Simp.neutralConfig
-   }
+private def getSimpUnfoldContext : MetaM Simp.Context := do
+   Simp.mkContext
+      (congrTheorems := (← getSimpCongrTheorems))
+      (config        := Simp.neutralConfig)
 
 def unfold (e : Expr) (declName : Name) : MetaM Simp.Result := do
   if let some unfoldThm ← getUnfoldEqnFor? declName  then

src/Lean/Meta/UnificationHint.lean

@@ -96,7 +96,7 @@ builtin_initialize
 
 def tryUnificationHints (t s : Expr) : MetaM Bool := do
   trace[Meta.isDefEq.hint] "{t} =?= {s}"
-  unless (← read).config.unificationHints do
+  unless (← getConfig).unificationHints do
     return false
   if t.isMVar then
     return false

src/Lean/Meta/WHNF.lean

@@ -529,7 +529,7 @@ private def whnfMatcher (e : Expr) : MetaM Expr := do
      TODO: consider other solutions; investigate whether the solution above produces counterintuitive behavior.  -/
   if (← getTransparency) matches .instances | .reducible then
     -- Also unfold some default-reducible constants; see `canUnfoldAtMatcher`
-    withTransparency .instances <| withReader (fun ctx => { ctx with canUnfold? := canUnfoldAtMatcher }) do
+    withTransparency .instances <| withCanUnfoldPred canUnfoldAtMatcher do
       whnf e
   else
     -- Do NOT use `canUnfoldAtMatcher` here as it does not affect all/default reducibility and inhibits caching (#2564).

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -1092,19 +1092,29 @@ def coeDelaborator : Delab := whenPPOption getPPCoercions do
   let e ← getExpr
   let .const declName _ := e.getAppFn | failure
   let some info ← Meta.getCoeFnInfo? declName | failure
+  let n := e.getAppNumArgs
+  guard <| n ≥ info.numArgs
   if (← getPPOption getPPExplicit) && info.coercee != 0 then
     -- Approximation: the only implicit arguments come before the coercee
     failure
-  let n := e.getAppNumArgs
-  withOverApp info.numArgs do
-    match info.type with
-    | .coe => `(↑$(← withNaryArg info.coercee delab))
-    | .coeFun =>
-      if n = info.numArgs then
-        `(⇑$(← withNaryArg info.coercee delab))
-      else
-        withNaryArg info.coercee delab
-    | .coeSort => `(↥$(← withNaryArg info.coercee delab))
+  if n == info.numArgs then
+    delabHead info 0 false
+  else
+    let nargs := n - info.numArgs
+    delabAppCore nargs (delabHead info nargs) (unexpand := false)
+where
+  delabHead (info : CoeFnInfo) (nargs : Nat) (insertExplicit : Bool) : Delab := do
+    guard <| !insertExplicit
+    if info.type == .coeFun && nargs > 0 then
+      -- In the CoeFun case, annotate with the coercee itself.
+      -- We can still see the whole coercion expression by hovering over the whitespace between the arguments.
+      withNaryArg info.coercee <| withAnnotateTermInfo delab
+    else
+      withAnnotateTermInfo do
+        match info.type with
+        | .coe     => `(↑$(← withNaryArg info.coercee delab))
+        | .coeFun  => `(⇑$(← withNaryArg info.coercee delab))
+        | .coeSort => `(↥$(← withNaryArg info.coercee delab))
 
 @[builtin_delab app.dite]
 def delabDIte : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPNotation <| withOverApp 5 do

src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean

@@ -205,7 +205,7 @@ def replaceLPsWithVars (e : Expr) : MetaM Expr := do
     | l => if !l.hasParam then some l else none
 
 def isDefEqAssigning (t s : Expr) : MetaM Bool := do
-  withReader (fun ctx => { ctx with config := { ctx.config with assignSyntheticOpaque := true }}) $
+  withConfig (fun cfg => { cfg with assignSyntheticOpaque := true }) do
     Meta.isDefEq t s
 
 def checkpointDefEq (t s : Expr) : MetaM Bool := do
@@ -624,7 +624,7 @@ open TopDownAnalyze SubExpr
 def topDownAnalyze (e : Expr) : MetaM OptionsPerPos := do
   let s₀ ← get
   withTraceNode `pp.analyze (fun _ => return e) do
-    withReader (fun ctx => { ctx with config := Elab.Term.setElabConfig ctx.config }) do
+    withConfig Elab.Term.setElabConfig do
       let ϕ : AnalyzeM OptionsPerPos := do withNewMCtxDepth analyze; pure (← get).annotations
       try
         let knowsType := getPPAnalyzeKnowsType (← getOptions)

src/Std.lean

@@ -6,5 +6,6 @@ Authors: Sebastian Ullrich
 prelude
 import Std.Data
 import Std.Sat
+import Std.Time
 import Std.Tactic
 import Std.Internal

src/Std/Data/DHashMap/Internal/WF.lean

@@ -38,7 +38,7 @@ theorem toListModel_mkArray_nil {c} :
 @[simp]
 theorem computeSize_eq {buckets : Array (AssocList α β)} :
     computeSize buckets = (toListModel buckets).length := by
-  rw [computeSize, toListModel, List.flatMap_eq_foldl, Array.foldl_eq_foldl_toList]
+  rw [computeSize, toListModel, List.flatMap_eq_foldl, Array.foldl_toList]
   suffices ∀ (l : List (AssocList α β)) (l' : List ((a : α) × β a)),
       l.foldl (fun d b => d + b.toList.length) l'.length =
         (l.foldl (fun acc a => acc ++ a.toList) l').length
@@ -61,13 +61,13 @@ theorem isEmpty_eq_isEmpty [BEq α] [Hashable α] {m : Raw α β} (h : Raw.WFImp
 
 theorem fold_eq {l : Raw α β} {f : γ → (a : α) → β a → γ} {init : γ} :
     l.fold f init = l.buckets.foldl (fun acc l => l.foldl f acc) init := by
-  simp only [Raw.fold, Raw.foldM, Array.foldlM_eq_foldlM_toList, Array.foldl_eq_foldl_toList,
+  simp only [Raw.fold, Raw.foldM, ← Array.foldlM_toList, Array.foldl_toList,
     ← List.foldl_eq_foldlM, Id.run, AssocList.foldl]
 
 theorem fold_cons_apply {l : Raw α β} {acc : List γ} (f : (a : α) → β a → γ) :
     l.fold (fun acc k v => f k v :: acc) acc =
       ((toListModel l.buckets).reverse.map (fun p => f p.1 p.2)) ++ acc := by
-  rw [fold_eq, Array.foldl_eq_foldl_toList, toListModel]
+  rw [fold_eq, ← Array.foldl_toList, toListModel]
   generalize l.buckets.toList = l
   induction l generalizing acc with
   | nil => simp

src/Std/Internal/Rat.lean

@@ -8,7 +8,8 @@ import Init.NotationExtra
 import Init.Data.ToString.Macro
 import Init.Data.Int.DivMod
 import Init.Data.Nat.Gcd
-namespace Lean
+namespace Std
+namespace Internal
 
 /-!
   Rational numbers for implementing decision procedures.
@@ -144,4 +145,5 @@ instance : Coe Int Rat where
   coe num := { num }
 
 end Rat
-end Lean
+end Internal
+end Std

src/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean

@@ -61,7 +61,7 @@ theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈
   | nil => cases h1
   | cons hd tl ih =>
     unfold DefaultClause.ofArray at h2
-    rw [Array.foldr_eq_foldr_toList, List.toArray_toList] at h2
+    rw [← Array.foldr_toList, List.toArray_toList] at h2
     dsimp only [List.foldr] at h2
     split at h2
     · cases h2
@@ -77,7 +77,7 @@ theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈
             · assumption
             · next heq _ _ =>
               unfold DefaultClause.ofArray
-              rw [Array.foldr_eq_foldr_toList, List.toArray_toList]
+              rw [← Array.foldr_toList, List.toArray_toList]
               exact heq
         · cases h1
           · simp only [← Option.some.inj h2]
@@ -89,7 +89,7 @@ theorem CNF.Clause.mem_lrat_of_mem (clause : CNF.Clause (PosFin n)) (h1 : l ∈
             apply ih
             assumption
             unfold DefaultClause.ofArray
-            rw [Array.foldr_eq_foldr_toList, List.toArray_toList]
+            rw [← Array.foldr_toList, List.toArray_toList]
             exact heq
 
 theorem CNF.Clause.convertLRAT_sat_of_sat (clause : CNF.Clause (PosFin n))

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean

@@ -106,7 +106,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
   constructor
   · simp only [ofArray]
   · have hsize : (ofArray arr).assignments.size = n := by
-      simp only [ofArray, Array.foldl_eq_foldl_toList]
+      simp only [ofArray, ← Array.foldl_toList]
       have hb : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray]
       have hl (acc : Array Assignment) (ih : acc.size = n) (cOpt : Option (DefaultClause n)) (_cOpt_in_arr : cOpt ∈ arr.toList) :
         (ofArray_fold_fn acc cOpt).size = n := by rw [size_ofArray_fold_fn acc cOpt, ih]
@@ -187,7 +187,7 @@ theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))
             exact ih i b h
     rcases List.foldlRecOn arr.toList ofArray_fold_fn (mkArray n unassigned) hb hl with ⟨_h_size, h'⟩
     intro i b h
-    simp only [ofArray, Array.foldl_eq_foldl_toList] at h
+    simp only [ofArray, ← Array.foldl_toList] at h
     exact h' i b h
 
 theorem readyForRatAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))) :
@@ -605,7 +605,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
 theorem readyForRupAdd_delete {n : Nat} (f : DefaultFormula n) (arr : Array Nat) :
     ReadyForRupAdd f → ReadyForRupAdd (delete f arr) := by
   intro h
-  rw [delete, Array.foldl_eq_foldl_toList]
+  rw [delete, ← Array.foldl_toList]
   constructor
   · have hb : f.rupUnits = #[] := h.1
     have hl (acc : DefaultFormula n) (ih : acc.rupUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.toList) :
@@ -625,7 +625,7 @@ theorem readyForRatAdd_delete {n : Nat} (f : DefaultFormula n) (arr : Array Nat)
     ReadyForRatAdd f → ReadyForRatAdd (delete f arr) := by
   intro h
   constructor
-  · rw [delete, Array.foldl_eq_foldl_toList]
+  · rw [delete, ← Array.foldl_toList]
     have hb : f.ratUnits = #[] := h.1
     have hl (acc : DefaultFormula n) (ih : acc.ratUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.toList) :
       (deleteOne acc id).ratUnits = #[] := by rw [deleteOne_preserves_ratUnits, ih]
@@ -659,7 +659,7 @@ theorem deleteOne_subset (f : DefaultFormula n) (id : Nat) (c : DefaultClause n)
 
 theorem delete_subset (f : DefaultFormula n) (arr : Array Nat) (c : DefaultClause n) :
     c ∈ toList (delete f arr) → c ∈ toList f := by
-  simp only [delete, Array.foldl_eq_foldl_toList]
+  simp only [delete, ← Array.foldl_toList]
   have hb : c ∈ toList f → c ∈ toList f := id
   have hl (f' : DefaultFormula n) (ih : c ∈ toList f' → c ∈ toList f) (id : Nat) (_ : id ∈ arr.toList) :
     c ∈ toList (deleteOne f' id) → c ∈ toList f := by intro h; exact ih <| deleteOne_subset f' id c h

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean

@@ -739,7 +739,7 @@ theorem size_assignemnts_confirmRupHint {n : Nat} (clauses : Array (Option (Defa
 theorem size_assignments_performRupCheck {n : Nat} (f : DefaultFormula n) (rupHints : Array Nat) :
     (performRupCheck f rupHints).1.assignments.size = f.assignments.size := by
   simp only [performRupCheck]
-  rw [Array.foldl_eq_foldl_toList]
+  rw [← Array.foldl_toList]
   have hb : (f.assignments, ([] : CNF.Clause (PosFin n)), false, false).1.size = f.assignments.size := rfl
   have hl (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool) (hsize : acc.1.size = f.assignments.size)
     (id : Nat) (_ : id ∈ rupHints.toList) : (confirmRupHint f.clauses acc id).1.size = f.assignments.size := by
@@ -1288,7 +1288,7 @@ theorem restoreAssignments_performRupCheck {n : Nat} (f : DefaultFormula n) (f_a
   have derivedLits_satisfies_invariant := derivedLitsInvariant_performRupCheck f f_assignments_size rupHints f'_assignments_size
   simp only at derivedLits_satisfies_invariant
   generalize (performRupCheck f rupHints).2.1 = derivedLits at *
-  rw [← f'_def, ← Array.foldl_eq_foldl_toList]
+  rw [← f'_def, Array.foldl_toList]
   let derivedLits_arr : Array (Literal (PosFin n)) := {toList := derivedLits}
   have derivedLits_arr_def : derivedLits_arr = {toList := derivedLits} := rfl
   have derivedLits_arr_nodup := nodup_derivedLits f f_assignments_size rupHints f'_assignments_size derivedLits
@@ -1301,7 +1301,7 @@ theorem restoreAssignments_performRupCheck {n : Nat} (f : DefaultFormula n) (f_a
     clear_insert_inductive_case f f_assignments_size derivedLits_arr derivedLits_arr_nodup idx assignments ih
   rcases Array.foldl_induction motive h_base h_inductive with ⟨h_size, h⟩
   apply Array.ext
-  · rw [Array.foldl_eq_foldl_toList, size_clearUnit_foldl f'.assignments clearUnit size_clearUnit derivedLits,
+  · rw [← Array.foldl_toList, size_clearUnit_foldl f'.assignments clearUnit size_clearUnit derivedLits,
       f'_assignments_size, f_assignments_size]
   · intro i hi1 hi2
     rw [f_assignments_size] at hi2

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean

@@ -544,7 +544,7 @@ theorem reduce_postcondition {n : Nat} (c : DefaultClause n) (assignment : Array
     (∀ l : Literal (PosFin n), reduce c assignment = reducedToUnit l → ∀ (p : (PosFin n) → Bool), p ⊨ assignment → p ⊨ c → p ⊨ l) := by
   let c_arr := c.clause.toArray
   have c_clause_rw : c.clause = c_arr.toList := by simp [c_arr]
-  rw [reduce, c_clause_rw, ← Array.foldl_eq_foldl_toList]
+  rw [reduce, c_clause_rw, Array.foldl_toList]
   let motive := ReducePostconditionInductionMotive c_arr assignment
   have h_base : motive 0 reducedToEmpty := by
     have : ∀ (a : PosFin n) (b : Bool), (reducedToEmpty = reducedToUnit (a, b)) = False := by intros; simp

src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean

@@ -99,17 +99,5 @@ attribute [bv_normalize] BitVec.mul_eq
 attribute [bv_normalize] BitVec.udiv_eq
 attribute [bv_normalize] BitVec.umod_eq
 
-@[bv_normalize]
-theorem Bool.and_eq_and (x y : Bool) : x.and y = (x && y) := by
-  rfl
-
-@[bv_normalize]
-theorem Bool.or_eq_or (x y : Bool) : x.or y = (x || y) := by
-  rfl
-
-@[bv_normalize]
-theorem Bool.no_eq_not (x : Bool) : x.not = !x := by
-  rfl
-
 end Normalize
 end Std.Tactic.BVDecide

src/Std/Tactic/BVDecide/Syntax.lean

@@ -29,6 +29,16 @@ structure BVDecideConfig where
   -/
   acNf : Bool := false
   /--
+  Split hypotheses of the form `h : (x && y) = true` into `h1 : x = true` and `h2 : y = true`.
+  This has synergy potential with embedded constraint substitution.
+  -/
+  andFlattening : Bool := true
+  /--
+  Look at all hypotheses of the form `h : x = true`, if `x` occurs in another hypothesis substitute
+  it with `true`.
+  -/
+  embeddedConstraintSubst : Bool := true
+  /--
   Output the AIG of bv_decide as graphviz into a file called aig.gv in the working directory of the
   Lean process.
   -/

src/Std/Time.lean

@@ -0,0 +1,231 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Std.Time.Time
+import Std.Time.Date
+import Std.Time.Zoned
+import Std.Time.Format
+import Std.Time.DateTime
+import Std.Time.Notation
+import Std.Time.Duration
+import Std.Time.Zoned.Database
+
+namespace Std
+namespace Time
+
+/-!
+# Time
+
+The Lean API for date, time, and duration functionalities.
+
+# Overview
+
+This module of the standard library defines various concepts related to time, such as dates, times,
+time zones and durations. These types are designed to be strongly-typed and to avoid problems with
+conversion. It offers both unbounded and bounded variants to suit different use cases, like
+adding days to a date or representing ordinal values.
+
+# Date and Time Components
+
+Date and time components are classified into different types based how you SHOULD use them. These
+components are categorized as:
+
+## Offset
+
+Offsets represent unbounded shifts in specific date or time units. They are typically used in operations
+like `date.addDays` where a `Day.Offset` is the parameter. Some offsets, such as `Month.Offset`, do not
+correspond directly to a specific duration in seconds, as their value depends on the context (if
+the year is leap or the size of the month). Offsets with a clear correspondent to seconds can be
+converted because they use an internal type called `UnitVal`.
+
+- Types with a correspondence to seconds:
+  - `Day.Offset`
+  - `Hour.Offset`
+  - `Week.Offset`
+  - `Millisecond.Offset`
+  - `Nanosecond.Offset`
+  - `Second.Offset`
+
+- Types without a correspondence to seconds:
+  - `Month.Offset`
+  - `Year.Offset`
+
+## Ordinal
+
+Ordinal types represent specific bounded values in reference to another unit, e.g., `Day.Ordinal`
+represents a day in a month, ranging from 1 to 31. Some ordinal types like `Hour.Ordinal` and `Second.Ordinal`,
+allow for values beyond the normal range (e.g, 60 seconds) to accommodate special cases with leap seconds
+like `23:59:60` that is valid in ISO 8601.
+
+- Ordinal types:
+  - `Day.Ordinal`: Ranges from 1 to 31.
+  - `Day.Ordinal.OfYear`: Ranges from 1 to (365 or 366).
+  - `Month.Ordinal`: Ranges from 1 to 12.
+  - `WeekOfYear.Ordinal`: Ranges from 1 to 53.
+  - `Hour.Ordinal`: Ranges from 0 to 23.
+  - `Millisecond.Ordinal`: Ranges from 0 to 999.
+  - `Minute.Ordinal`: Ranges from 0 to 59.
+  - `Nanosecond.Ordinal`: Ranges from 0 to 999,999,999.
+  - `Second.Ordinal`: Ranges from 0 to 60.
+  - `Weekday`: That is a inductive type with all the seven days.
+
+## Span
+
+Span types are used as subcomponents of other types. They represent a range of values in the limits
+of the parent type, e.g, `Nanosecond.Span` ranges from -999,999,999 to 999,999,999, as 1,000,000,000
+nanoseconds corresponds to one second.
+
+- Span types:
+  - `Nanosecond.Span`: Ranges from -999,999,999 to 999,999,999.
+
+# Date and Time Types
+
+Dates and times are made up of different parts. An `Ordinal` is an absolute value, like a specific day in a month,
+while an `Offset` is a shift forward or backward in time, used in arithmetic operations to add or subtract days, months or years.
+Dates use components like `Year.Ordinal`, `Month.Ordinal`, and `Day.Ordinal` to ensure they represent
+valid points in time.
+
+Some types, like `Duration`, include a `Span` to represent ranges over other types, such as `Second.Offset`.
+This type can have a fractional nanosecond part that can be negative or positive that is represented as a `Nanosecond.Span`.
+
+## Date
+These types provide precision down to the day level, useful for representing and manipulating dates.
+
+- **`PlainDate`:** Represents a calendar date in the format `YYYY-MM-DD`.
+
+## Time
+These types offer precision down to the nanosecond level, useful for representing and manipulating time of day.
+
+- **`PlainTime`**: Represents a time of day in the format `HH:mm:ss,sssssssss`.
+
+## Date and time
+Combines date and time into a single representation, useful for precise timestamps and scheduling.
+
+- **`PlainDateTime`**: Represents both date and time in the format `YYYY-MM-DDTHH:mm:ss,sssssssss`.
+- **`Timestamp`**: Represents a specific point in time with nanosecond precision. Its zero value corresponds
+to the UNIX epoch. This type should be used when sending or receiving timestamps between systems.
+
+## Zoned date and times.
+Combines date, time and time zones.
+
+- **`DateTime`**: Represents both date and time but with a time zone in the type constructor.
+- **`ZonedDateTime`**: Is a way to represent date and time that includes `ZoneRules`, which consider
+Daylight Saving Time (DST). This means it can handle local time changes throughout the year better
+than a regular `DateTime`. If you want to use a specific time zone without worrying about DST, you can
+use the `ofTimestampWithZone` function, which gives you a `ZonedDateTime` based only on that time zone,
+without considering the zone rules, otherwise you can use `ofTimestamp` or `ofTimestampWithIdentifier`.
+
+## Duration
+Represents spans of time and the difference between two points in time.
+
+- **`Duration`**: Represents the time span or difference between two `Timestamp`s values with nanosecond precision.
+
+# Formats
+
+Format strings are used to convert between `String` representations and date/time types, like `yyyy-MM-dd'T'HH:mm:ss.sssZ`.
+The table below shows the available format specifiers. Some specifiers can be repeated to control truncation or offsets.
+When a character is repeated `n` times, it usually truncates the value to `n` characters.
+
+The supported formats include:
+- `G`: Represents the era, such as AD (Anno Domini) or BC (Before Christ).
+  - `G`, `GG`, `GGG` (short): Displays the era in a short format (e.g., "AD").
+  - `GGGG` (full): Displays the era in a full format (e.g., "Anno Domini").
+  - `GGGGG` (narrow): Displays the era in a narrow format (e.g., "A").
+- `y`: Represents the year of the era.
+  - `yy`: Displays the year in a two-digit format, showing the last two digits (e.g., "04" for 2004).
+  - `yyyy`: Displays the year in a four-digit format (e.g., "2004").
+  - `yyyy+`: Extended format for years with more than four digits.
+- `u`: Represents the year.
+  - `uu`: Two-digit year format, showing the last two digits (e.g., "04" for 2004).
+  - `uuuu`: Displays the year in a four-digit format (e.g., "2004" or "-1000").
+  - `uuuu+`: Extended format for handling years with more than four digits (e.g., "12345" or "-12345"). Useful for historical dates far into the past or future!
+- `D`: Represents the day of the year.
+- `M`: Represents the month of the year, displayed as either a number or text.
+  - `M`, `MM`: Displays the month as a number, with `MM` zero-padded (e.g., "7" for July, "07" for July with padding).
+  - `MMM`: Displays the abbreviated month name (e.g., "Jul").
+  - `MMMM`: Displays the full month name (e.g., "July").
+  - `MMMMM`: Displays the month in a narrow form (e.g., "J" for July).
+- `d`: Represents the day of the month.
+- `Q`: Represents the quarter of the year.
+  - `Q`, `QQ`: Displays the quarter as a number (e.g., "3", "03").
+  - `QQQ` (short): Displays the quarter as an abbreviated text (e.g., "Q3").
+  - `QQQQ` (full): Displays the full quarter text (e.g., "3rd quarter").
+  - `QQQQQ` (narrow): Displays the quarter as a short number (e.g., "3").
+- `w`: Represents the week of the week-based year, each week starts on Monday (e.g., "27").
+- `W`: Represents the week of the month, each week starts on Monday (e.g., "4").
+- `E`: Represents the day of the week as text.
+  - `E`, `EE`, `EEE`: Displays the abbreviated weekday name (e.g., "Tue").
+  - `EEEE`: Displays the full day name (e.g., "Tuesday").
+  - `EEEEE`: Displays the narrow day name (e.g., "T" for Tuesday).
+- `e`: Represents the weekday as number or text.
+  - `e`, `ee`: Displays the the as a number, starting from 1 (Monday) to 7 (Sunday).
+  - `eee`, `eeee`, `eeeee`: Displays the weekday as text (same format as `E`).
+- `F`: Represents the week of the month that the first week starts on the first day of the month (e.g., "3").
+- `a`: Represents the AM or PM designation of the day.
+  - `a`, `aa`, `aaa`: Displays AM or PM in a concise format (e.g., "PM").
+  - `aaaa`: Displays the full AM/PM designation (e.g., "Post Meridium").
+- `h`: Represents the hour of the AM/PM clock (1-12) (e.g., "12").
+  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
+- `K`: Represents the hour of the AM/PM clock (0-11) (e.g., "0").
+  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
+- `k`: Represents the hour of the day in a 1-24 format (e.g., "24").
+  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
+- `H`: Represents the hour of the day in a 0-23 format (e.g., "0").
+  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
+- `m`: Represents the minute of the hour (e.g., "30").
+  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
+- `s`: Represents the second of the minute (e.g., "55").
+  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
+- `S`: Represents a fraction of a second, typically displayed as a decimal number (e.g., "978" for milliseconds).
+  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
+- `A`: Represents the millisecond of the day (e.g., "1234").
+  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
+- `n`: Represents the nanosecond of the second (e.g., "987654321").
+  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
+- `N`: Represents the nanosecond of the day (e.g., "1234000000").
+  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
+- `VV`: Represents the time zone ID, which could be a city-based zone (e.g., "America/Los_Angeles"), a UTC marker (`"Z"`), or a specific offset (e.g., "-08:30").
+  - One or more repetitions of the character indicates the truncation of the value to the specified number of characters.
+- `z`: Represents the time zone name.
+  - `z`, `zz`, `zzz`: Shows an abbreviated time zone name (e.g., "PST" for Pacific Standard Time).
+  - `zzzz`: Displays the full time zone name (e.g., "Pacific Standard Time").
+- `O`: Represents the localized zone offset in the format "GMT" followed by the time difference from UTC.
+  - `O`: Displays the GMT offset in a simple format (e.g., "GMT+8").
+  - `OOOO`: Displays the full GMT offset, including hours and minutes (e.g., "GMT+08:00").
+- `X`: Represents the zone offset. It uses 'Z' for UTC and can represent any offset (positive or negative).
+  - `X`: Displays the hour offset (e.g., "-08").
+  - `XX`: Displays the hour and minute offset without a colon (e.g., "-0830").
+  - `XXX`: Displays the hour and minute offset with a colon (e.g., "-08:30").
+  - `XXXX`: Displays the hour, minute, and second offset without a colon (e.g., "-083045").
+  - `XXXXX`: Displays the hour, minute, and second offset with a colon (e.g., "-08:30:45").
+- `x`: Represents the zone offset. Similar to X, but does not display 'Z' for UTC and focuses only on positive offsets.
+  - `x`: Displays the hour offset (e.g., "+08").
+  - `xx`: Displays the hour and minute offset without a colon (e.g., "+0830").
+  - `xxx`: Displays the hour and minute offset with a colon (e.g., "+08:30").
+  - `xxxx`: Displays the hour, minute, and second offset without a colon (e.g., "+083045").
+  - `xxxxx`: Displays the hour, minute, and second offset with a colon (e.g., "+08:30:45").
+- `Z`: Always includes an hour and minute offset and may use 'Z' for UTC, providing clear differentiation between UTC and other time zones.
+  - `Z`: Displays the hour and minute offset without a colon (e.g., "+0800").
+  - `ZZ`: Displays "GMT" followed by the time offset (e.g., "GMT+08:00" or "Z").
+  - `ZZZ`: Displays the full hour, minute, and second offset with a colon (e.g., "+08:30:45" or "Z").
+
+# Macros
+
+In order to help the user build dates easily, there are a lot of macros available for creating dates.
+The `.sssssssss` can be ommited in most cases.
+
+
+- **`date("uuuu-MM-dd")`**: Represents a date in the `uuuu-MM-dd` format, where `uuuu` refers to the year.
+- **`time("HH:mm:ss.sssssssss")`**: Represents a time in the format `HH:mm:ss.sssssssss`, including optional support for nanoseconds.
+- **`datetime("uuuu-MM-ddTHH:mm:ss.sssssssss")`**: Represents a datetime value in the `uuuu-MM-ddTHH:mm:ss.sssssssss` format, with optional nanoseconds.
+- **`offset("+HH:mm")`**: Represents a timezone offset in the format `+HH:mm`, where `+` or `-` indicates the direction from UTC.
+- **`timezone("NAME/ID ZZZ")`**: Specifies a timezone using a region-based name or ID, along with its associated offset.
+- **`datespec("FORMAT")`**: Defines a compile-time date format based on the provided string.
+- **`zoned("uuuu-MM-ddTHH:mm:ss.sssssssssZZZ")`**: Represents a `ZonedDateTime` with a fixed timezone and optional nanosecond precision.
+- **`zoned("uuuu-MM-ddTHH:mm:ss.sssssssss[IDENTIFIER]")`**: Defines an `IO ZonedDateTime`, where the timezone identifier is dynamically retrieved from the default timezone database.
+- **`zoned("uuuu-MM-ddTHH:mm:ss.sssssssss, timezone")`**: Represents an `IO ZonedDateTime`, using a specified `timezone` term and allowing optional nanoseconds.
+
+-/

src/Std/Time/Date.lean

@@ -0,0 +1,8 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Std.Time.Date.Basic
+import Std.Time.Date.PlainDate

src/Std/Time/Date/Basic.lean

@@ -0,0 +1,476 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Std.Time.Date.Unit.Basic
+import Std.Time.Date.ValidDate
+import Std.Time.Time.Basic
+
+namespace Std
+namespace Time
+
+namespace Nanosecond
+namespace Offset
+
+/--
+Convert `Nanosecond.Offset` into `Day.Offset`.
+-/
+@[inline]
+def toDays (nanoseconds : Nanosecond.Offset) : Day.Offset :=
+  nanoseconds.div 86400000000000
+
+/--
+Convert `Day.Offset` into `Nanosecond.Offset`.
+-/
+@[inline]
+def ofDays (days : Day.Offset) : Nanosecond.Offset :=
+  days.mul 86400000000000
+
+/--
+Convert `Nanosecond.Offset` into `Week.Offset`.
+-/
+@[inline]
+def toWeeks (nanoseconds : Nanosecond.Offset) : Week.Offset :=
+  nanoseconds.div 604800000000000
+
+/--
+Convert `Week.Offset` into `Nanosecond.Offset`.
+-/
+@[inline]
+def ofWeeks (weeks : Week.Offset) : Nanosecond.Offset :=
+  weeks.mul 604800000000000
+
+end Offset
+end Nanosecond
+
+namespace Millisecond
+namespace Offset
+
+/--
+Convert `Millisecond.Offset` into `Day.Offset`.
+-/
+@[inline]
+def toDays (milliseconds : Millisecond.Offset) : Day.Offset :=
+  milliseconds.div 86400000
+
+/--
+Convert `Day.Offset` into `Millisecond.Offset`.
+-/
+@[inline]
+def ofDays (days : Day.Offset) : Millisecond.Offset :=
+  days.mul 86400000
+
+/--
+Convert `Millisecond.Offset` into `Week.Offset`.
+-/
+@[inline]
+def toWeeks (milliseconds : Millisecond.Offset) : Week.Offset :=
+  milliseconds.div 604800000
+
+/--
+Convert `Week.Offset` into `Millisecond.Offset`.
+-/
+@[inline]
+def ofWeeks (weeks : Week.Offset) : Millisecond.Offset :=
+  weeks.mul 604800000
+
+end Offset
+end Millisecond
+
+namespace Second
+namespace Offset
+
+/--
+Convert `Second.Offset` into `Day.Offset`.
+-/
+@[inline]
+def toDays (seconds : Second.Offset) : Day.Offset :=
+  seconds.div 86400
+
+/--
+Convert `Day.Offset` into `Second.Offset`.
+-/
+@[inline]
+def ofDays (days : Day.Offset) : Second.Offset :=
+  days.mul 86400
+
+/--
+Convert `Second.Offset` into `Week.Offset`.
+-/
+@[inline]
+def toWeeks (seconds : Second.Offset) : Week.Offset :=
+  seconds.div 604800
+
+/--
+Convert `Week.Offset` into `Second.Offset`.
+-/
+@[inline]
+def ofWeeks (weeks : Week.Offset) : Second.Offset :=
+  weeks.mul 604800
+
+end Offset
+end Second
+
+namespace Minute
+namespace Offset
+
+/--
+Convert `Minute.Offset` into `Day.Offset`.
+-/
+@[inline]
+def toDays (minutes : Minute.Offset) : Day.Offset :=
+  minutes.div 1440
+
+/--
+Convert `Day.Offset` into `Minute.Offset`.
+-/
+@[inline]
+def ofDays (days : Day.Offset) : Minute.Offset :=
+  days.mul 1440
+
+/--
+Convert `Minute.Offset` into `Week.Offset`.
+-/
+@[inline]
+def toWeeks (minutes : Minute.Offset) : Week.Offset :=
+  minutes.div 10080
+
+/--
+Convert `Week.Offset` into `Minute.Offset`.
+-/
+@[inline]
+def ofWeeks (weeks : Week.Offset) : Minute.Offset :=
+  weeks.mul 10080
+
+end Offset
+end Minute
+
+namespace Hour
+namespace Offset
+
+/--
+Convert `Hour.Offset` into `Day.Offset`.
+-/
+@[inline]
+def toDays (hours : Hour.Offset) : Day.Offset :=
+  hours.div 24
+
+/--
+Convert `Day.Offset` into `Hour.Offset`.
+-/
+@[inline]
+def ofDays (days : Day.Offset) : Hour.Offset :=
+  days.mul 24
+
+/--
+Convert `Hour.Offset` into `Week.Offset`.
+-/
+@[inline]
+def toWeeks (hours : Hour.Offset) : Week.Offset :=
+  hours.div 168
+
+/--
+Convert `Week.Offset` into `Hour.Offset`.
+-/
+@[inline]
+def ofWeeks (weeks : Week.Offset) : Hour.Offset :=
+  weeks.mul 168
+
+end Offset
+end Hour
+
+instance : HAdd Nanosecond.Offset Nanosecond.Offset Nanosecond.Offset where
+  hAdd x y := x.add y
+
+instance : HAdd Nanosecond.Offset Millisecond.Offset Nanosecond.Offset where
+  hAdd x y := x.add y.toNanoseconds
+
+instance : HAdd Nanosecond.Offset Second.Offset Nanosecond.Offset where
+  hAdd x y := x.add y.toNanoseconds
+
+instance : HAdd Nanosecond.Offset Minute.Offset Nanosecond.Offset where
+  hAdd x y := x.add y.toNanoseconds
+
+instance : HAdd Nanosecond.Offset Hour.Offset Nanosecond.Offset where
+  hAdd x y := x.add y.toNanoseconds
+
+instance : HAdd Nanosecond.Offset Day.Offset Nanosecond.Offset where
+  hAdd x y := x.add y.toNanoseconds
+
+instance : HAdd Nanosecond.Offset Week.Offset Nanosecond.Offset where
+  hAdd x y := x.add y.toNanoseconds
+
+instance : HAdd Millisecond.Offset Nanosecond.Offset Nanosecond.Offset where
+  hAdd x y := x.toNanoseconds.add y
+
+instance : HAdd Millisecond.Offset Millisecond.Offset Millisecond.Offset where
+  hAdd x y := x.add y
+
+instance : HAdd Millisecond.Offset Second.Offset Millisecond.Offset where
+  hAdd x y := x.add y.toMilliseconds
+
+instance : HAdd Millisecond.Offset Minute.Offset Millisecond.Offset where
+  hAdd x y := x.add y.toMilliseconds
+
+instance : HAdd Millisecond.Offset Hour.Offset Millisecond.Offset where
+  hAdd x y := x.add y.toMilliseconds
+
+instance : HAdd Millisecond.Offset Day.Offset Millisecond.Offset where
+  hAdd x y := x.add y.toMilliseconds
+
+instance : HAdd Millisecond.Offset Week.Offset Millisecond.Offset where
+  hAdd x y := x.add y.toMilliseconds
+
+instance : HAdd Second.Offset Nanosecond.Offset Nanosecond.Offset where
+  hAdd x y := x.toNanoseconds.add y
+
+instance : HAdd Second.Offset Millisecond.Offset Millisecond.Offset where
+  hAdd x y := x.toMilliseconds.add y
+
+instance : HAdd Second.Offset Second.Offset Second.Offset where
+  hAdd x y := x.add y
+
+instance : HAdd Second.Offset Minute.Offset Second.Offset where
+  hAdd x y := x.add y.toSeconds
+
+instance : HAdd Second.Offset Hour.Offset Second.Offset where
+  hAdd x y := x.add y.toSeconds
+
+instance : HAdd Second.Offset Day.Offset Second.Offset where
+  hAdd x y := x.add y.toSeconds
+
+instance : HAdd Second.Offset Week.Offset Second.Offset where
+  hAdd x y := x.add y.toSeconds
+
+instance : HAdd Minute.Offset Nanosecond.Offset Nanosecond.Offset where
+  hAdd x y := x.toNanoseconds.add y
+
+instance : HAdd Minute.Offset Millisecond.Offset Millisecond.Offset where
+  hAdd x y := x.toMilliseconds.add y
+
+instance : HAdd Minute.Offset Second.Offset Second.Offset where
+  hAdd x y := x.toSeconds.add y
+
+instance : HAdd Minute.Offset Minute.Offset Minute.Offset where
+  hAdd x y := x.add y
+
+instance : HAdd Minute.Offset Hour.Offset Minute.Offset where
+  hAdd x y := x.add y.toMinutes
+
+instance : HAdd Minute.Offset Day.Offset Minute.Offset where
+  hAdd x y := x.add y.toMinutes
+
+instance : HAdd Minute.Offset Week.Offset Minute.Offset where
+  hAdd x y := x.add y.toMinutes
+
+instance : HAdd Hour.Offset Nanosecond.Offset Nanosecond.Offset where
+  hAdd x y := x.toNanoseconds.add y
+
+instance : HAdd Hour.Offset Millisecond.Offset Millisecond.Offset where
+  hAdd x y := x.toMilliseconds.add y
+
+instance : HAdd Hour.Offset Second.Offset Second.Offset where
+  hAdd x y := x.toSeconds.add y
+
+instance : HAdd Hour.Offset Minute.Offset Minute.Offset where
+  hAdd x y := x.toMinutes.add y
+
+instance : HAdd Hour.Offset Hour.Offset Hour.Offset where
+  hAdd x y := x.add y
+
+instance : HAdd Hour.Offset Day.Offset Hour.Offset where
+  hAdd x y := x.add y.toHours
+
+instance : HAdd Hour.Offset Week.Offset Hour.Offset where
+  hAdd x y := x.add y.toHours
+
+instance : HAdd Day.Offset Nanosecond.Offset Nanosecond.Offset where
+  hAdd x y := x.toNanoseconds.add y
+
+instance : HAdd Day.Offset Millisecond.Offset Millisecond.Offset where
+  hAdd x y := x.toMilliseconds.add y
+
+instance : HAdd Day.Offset Second.Offset Second.Offset where
+  hAdd x y := x.toSeconds.add y
+
+instance : HAdd Day.Offset Minute.Offset Minute.Offset where
+  hAdd x y := x.toMinutes.add y
+
+instance : HAdd Day.Offset Hour.Offset Hour.Offset where
+  hAdd x y := x.toHours.add y
+
+instance : HAdd Day.Offset Day.Offset Day.Offset where
+  hAdd x y := x.add y
+
+instance : HAdd Day.Offset Week.Offset Day.Offset where
+  hAdd x y := x.add y.toDays
+
+instance : HAdd Week.Offset Nanosecond.Offset Nanosecond.Offset where
+  hAdd x y := x.toNanoseconds.add y
+
+instance : HAdd Week.Offset Millisecond.Offset Millisecond.Offset where
+  hAdd x y := x.toMilliseconds.add y
+
+instance : HAdd Week.Offset Second.Offset Second.Offset where
+  hAdd x y := x.toSeconds.add y
+
+instance : HAdd Week.Offset Minute.Offset Minute.Offset where
+  hAdd x y := x.toMinutes.add y
+
+instance : HAdd Week.Offset Hour.Offset Hour.Offset where
+  hAdd x y := x.toHours.add y
+
+instance : HAdd Week.Offset Day.Offset Day.Offset where
+  hAdd x y := x.toDays.add y
+
+instance : HAdd Week.Offset Week.Offset Week.Offset where
+  hAdd x y := x.add y
+
+instance : HSub Nanosecond.Offset Nanosecond.Offset Nanosecond.Offset where
+  hSub x y := x.sub y
+
+instance : HSub Nanosecond.Offset Millisecond.Offset Nanosecond.Offset where
+  hSub x y := x.sub y.toNanoseconds
+
+instance : HSub Nanosecond.Offset Second.Offset Nanosecond.Offset where
+  hSub x y := x.sub y.toNanoseconds
+
+instance : HSub Nanosecond.Offset Minute.Offset Nanosecond.Offset where
+  hSub x y := x.sub y.toNanoseconds
+
+instance : HSub Nanosecond.Offset Hour.Offset Nanosecond.Offset where
+  hSub x y := x.sub y.toNanoseconds
+
+instance : HSub Nanosecond.Offset Day.Offset Nanosecond.Offset where
+  hSub x y := x.sub y.toNanoseconds
+
+instance : HSub Nanosecond.Offset Week.Offset Nanosecond.Offset where
+  hSub x y := x.sub y.toNanoseconds
+
+instance : HSub Millisecond.Offset Nanosecond.Offset Nanosecond.Offset where
+  hSub x y := x.toNanoseconds.sub y
+
+instance : HSub Millisecond.Offset Millisecond.Offset Millisecond.Offset where
+  hSub x y := x.sub y
+
+instance : HSub Millisecond.Offset Second.Offset Millisecond.Offset where
+  hSub x y := x.sub y.toMilliseconds
+
+instance : HSub Millisecond.Offset Minute.Offset Millisecond.Offset where
+  hSub x y := x.sub y.toMilliseconds
+
+instance : HSub Millisecond.Offset Hour.Offset Millisecond.Offset where
+  hSub x y := x.sub y.toMilliseconds
+
+instance : HSub Millisecond.Offset Day.Offset Millisecond.Offset where
+  hSub x y := x.sub y.toMilliseconds
+
+instance : HSub Millisecond.Offset Week.Offset Millisecond.Offset where
+  hSub x y := x.sub y.toMilliseconds
+
+instance : HSub Second.Offset Nanosecond.Offset Nanosecond.Offset where
+  hSub x y := x.toNanoseconds.sub y
+
+instance : HSub Second.Offset Millisecond.Offset Millisecond.Offset where
+  hSub x y := x.toMilliseconds.sub y
+
+instance : HSub Second.Offset Second.Offset Second.Offset where
+  hSub x y := x.sub y
+
+instance : HSub Second.Offset Minute.Offset Second.Offset where
+  hSub x y := x.sub y.toSeconds
+
+instance : HSub Second.Offset Hour.Offset Second.Offset where
+  hSub x y := x.sub y.toSeconds
+
+instance : HSub Second.Offset Day.Offset Second.Offset where
+  hSub x y := x.sub y.toSeconds
+
+instance : HSub Second.Offset Week.Offset Second.Offset where
+  hSub x y := x.sub y.toSeconds
+
+instance : HSub Minute.Offset Nanosecond.Offset Nanosecond.Offset where
+  hSub x y := x.toNanoseconds.sub y
+
+instance : HSub Minute.Offset Millisecond.Offset Millisecond.Offset where
+  hSub x y := x.toMilliseconds.sub y
+
+instance : HSub Minute.Offset Second.Offset Second.Offset where
+  hSub x y := x.toSeconds.sub y
+
+instance : HSub Minute.Offset Minute.Offset Minute.Offset where
+  hSub x y := x.sub y
+
+instance : HSub Minute.Offset Hour.Offset Minute.Offset where
+  hSub x y := x.sub y.toMinutes
+
+instance : HSub Minute.Offset Day.Offset Minute.Offset where
+  hSub x y := x.sub y.toMinutes
+
+instance : HSub Minute.Offset Week.Offset Minute.Offset where
+  hSub x y := x.sub y.toMinutes
+
+instance : HSub Hour.Offset Nanosecond.Offset Nanosecond.Offset where
+  hSub x y := x.toNanoseconds.sub y
+
+instance : HSub Hour.Offset Millisecond.Offset Millisecond.Offset where
+  hSub x y := x.toMilliseconds.sub y
+
+instance : HSub Hour.Offset Second.Offset Second.Offset where
+  hSub x y := x.toSeconds.sub y
+
+instance : HSub Hour.Offset Minute.Offset Minute.Offset where
+  hSub x y := x.toMinutes.sub y
+
+instance : HSub Hour.Offset Hour.Offset Hour.Offset where
+  hSub x y := x.sub y
+
+instance : HSub Hour.Offset Day.Offset Hour.Offset where
+  hSub x y := x.sub y.toHours
+
+instance : HSub Hour.Offset Week.Offset Hour.Offset where
+  hSub x y := x.sub y.toHours
+
+instance : HSub Day.Offset Nanosecond.Offset Nanosecond.Offset where
+  hSub x y := x.toNanoseconds.sub y
+
+instance : HSub Day.Offset Millisecond.Offset Millisecond.Offset where
+  hSub x y := x.toMilliseconds.sub y
+
+instance : HSub Day.Offset Second.Offset Second.Offset where
+  hSub x y := x.toSeconds.sub y
+
+instance : HSub Day.Offset Minute.Offset Minute.Offset where
+  hSub x y := x.toMinutes.sub y
+
+instance : HSub Day.Offset Hour.Offset Hour.Offset where
+  hSub x y := x.toHours.sub y
+
+instance : HSub Day.Offset Day.Offset Day.Offset where
+  hSub x y := x.sub y
+
+instance : HSub Day.Offset Week.Offset Day.Offset where
+  hSub x y := x.sub y.toDays
+
+instance : HSub Week.Offset Nanosecond.Offset Nanosecond.Offset where
+  hSub x y := x.toNanoseconds.sub y
+
+instance : HSub Week.Offset Millisecond.Offset Millisecond.Offset where
+  hSub x y := x.toMilliseconds.sub y
+
+instance : HSub Week.Offset Second.Offset Second.Offset where
+  hSub x y := x.toSeconds.sub y
+
+instance : HSub Week.Offset Minute.Offset Minute.Offset where
+  hSub x y := x.toMinutes.sub y
+
+instance : HSub Week.Offset Hour.Offset Hour.Offset where
+  hSub x y := x.toHours.sub y
+
+instance : HSub Week.Offset Day.Offset Day.Offset where
+  hSub x y := x.toDays.sub y
+
+instance : HSub Week.Offset Week.Offset Week.Offset where
+  hSub x y := x.sub y

src/Std/Time/Date/PlainDate.lean

@@ -0,0 +1,354 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Std.Time.Internal
+import Std.Time.Date.Basic
+import Std.Internal.Rat
+
+namespace Std
+namespace Time
+open Std.Internal
+open Std.Time
+open Internal
+open Lean
+
+set_option linter.all true
+
+/--
+`PlainDate` represents a date in the Year-Month-Day (YMD) format. It encapsulates the year, month,
+and day components, with validation to ensure the date is valid.
+-/
+structure PlainDate where
+
+  /-- The year component of the date. It is represented as an `Offset` type from `Year`. -/
+  year : Year.Offset
+
+  /-- The month component of the date. It is represented as an `Ordinal` type from `Month`. -/
+  month : Month.Ordinal
+
+  /-- The day component of the date. It is represented as an `Ordinal` type from `Day`. -/
+  day : Day.Ordinal
+
+  /-- Validates the date by ensuring that the year, month, and day form a correct and valid date. -/
+  valid : year.Valid month day
+  deriving Repr
+
+instance : Inhabited PlainDate where
+  default := ⟨1, 1, 1, by decide⟩
+
+instance : BEq PlainDate where
+  beq x y := x.day == y.day && x.month == y.month && x.year == y.year
+
+namespace PlainDate
+
+/--
+Creates a `PlainDate` by clipping the day to ensure validity. This function forces the date to be
+valid by adjusting the day to fit within the valid range to fit the given month and year.
+-/
+@[inline]
+def ofYearMonthDayClip (year : Year.Offset) (month : Month.Ordinal) (day : Day.Ordinal) : PlainDate :=
+  let day := month.clipDay year.isLeap day
+  PlainDate.mk year month day Month.Ordinal.valid_clipDay
+
+instance : Inhabited PlainDate where
+  default := mk 0 1 1 (by decide)
+
+/--
+Creates a new `PlainDate` from year, month, and day components.
+-/
+@[inline]
+def ofYearMonthDay? (year : Year.Offset) (month : Month.Ordinal) (day : Day.Ordinal) : Option PlainDate :=
+  if valid : year.Valid month day
+    then some (PlainDate.mk year month day valid)
+    else none
+
+/--
+Creates a `PlainDate` from a year and a day ordinal within that year.
+-/
+@[inline]
+def ofYearOrdinal (year : Year.Offset) (ordinal : Day.Ordinal.OfYear year.isLeap) : PlainDate :=
+  let ⟨⟨month, day⟩, proof⟩ := ValidDate.ofOrdinal ordinal
+  ⟨year, month, day, proof⟩
+
+/--
+Creates a `PlainDate` from the number of days since the UNIX epoch (January 1st, 1970).
+-/
+def ofDaysSinceUNIXEpoch (day : Day.Offset) : PlainDate :=
+  let z := day.toInt + 719468
+  let era := (if z ≥ 0 then z else z - 146096).tdiv 146097
+  let doe := z - era * 146097
+  let yoe := (doe - doe.tdiv 1460 + doe.tdiv 36524 - doe.tdiv 146096).tdiv 365
+  let y := yoe + era * 400
+  let doy := doe - (365 * yoe + yoe.tdiv 4 - yoe.tdiv 100)
+  let mp := (5 * doy + 2).tdiv 153
+  let d := doy - (153 * mp + 2).tdiv 5 + 1
+  let m := mp + (if mp < 10 then 3 else -9)
+  let y := y + (if m <= 2 then 1 else 0)
+  .ofYearMonthDayClip y (.clip m (by decide)) (.clip d (by decide))
+
+/--
+Returns the unaligned week of the month for a `PlainDate` (day divided by 7, plus 1).
+-/
+def weekOfMonth (date : PlainDate) : Bounded.LE 1 5 :=
+  date.day.sub 1 |>.ediv 7 (by decide) |>.add 1
+
+/--
+Determines the quarter of the year for the given `PlainDate`.
+-/
+def quarter (date : PlainDate) : Bounded.LE 1 4 :=
+  date.month.sub 1 |>.ediv 3 (by decide) |>.add 1
+
+/--
+Transforms a `PlainDate` into a `Day.Ordinal.OfYear`.
+-/
+def dayOfYear (date : PlainDate) : Day.Ordinal.OfYear date.year.isLeap :=
+  ValidDate.dayOfYear ⟨(date.month, date.day), date.valid⟩
+
+/--
+Determines the era of the given `PlainDate` based on its year.
+-/
+@[inline]
+def era (date : PlainDate) : Year.Era :=
+  date.year.era
+
+/--
+Checks if the `PlainDate` is in a leap year.
+-/
+@[inline]
+def inLeapYear (date : PlainDate) : Bool :=
+  date.year.isLeap
+
+/--
+Converts a `PlainDate` to the number of days since the UNIX epoch.
+-/
+def toDaysSinceUNIXEpoch (date : PlainDate) : Day.Offset :=
+  let y : Int := if date.month.toInt > 2 then date.year else date.year.toInt - 1
+  let era : Int := (if y ≥ 0 then y else y - 399).tdiv 400
+  let yoe : Int := y - era * 400
+  let m : Int := date.month.toInt
+  let d : Int := date.day.toInt
+  let doy := (153 * (m + (if m > 2 then -3 else 9)) + 2).tdiv 5 + d - 1
+  let doe := yoe * 365 + yoe.tdiv 4 - yoe.tdiv 100 + doy
+
+  .ofInt (era * 146097 + doe - 719468)
+
+/--
+Adds a given number of days to a `PlainDate`.
+-/
+@[inline]
+def addDays (date : PlainDate) (days : Day.Offset) : PlainDate :=
+  let dateDays := date.toDaysSinceUNIXEpoch
+  ofDaysSinceUNIXEpoch (dateDays + days)
+
+/--
+Subtracts a given number of days from a `PlainDate`.
+-/
+@[inline]
+def subDays (date : PlainDate) (days : Day.Offset) : PlainDate :=
+  addDays date (-days)
+
+/--
+Adds a given number of weeks to a `PlainDate`.
+-/
+@[inline]
+def addWeeks (date : PlainDate) (weeks : Week.Offset) : PlainDate :=
+  let dateDays := date.toDaysSinceUNIXEpoch
+  let daysToAdd := weeks.toDays
+  ofDaysSinceUNIXEpoch (dateDays + daysToAdd)
+
+/--
+Subtracts a given number of weeks from a `PlainDate`.
+-/
+@[inline]
+def subWeeks (date : PlainDate) (weeks : Week.Offset) : PlainDate :=
+  addWeeks date (-weeks)
+
+/--
+Adds a given number of months to a `PlainDate`, clipping the day to the last valid day of the month.
+-/
+def addMonthsClip (date : PlainDate) (months : Month.Offset) : PlainDate :=
+  let totalMonths := (date.month.toOffset - 1) + months
+  let totalMonths : Int := totalMonths
+  let wrappedMonths := Bounded.LE.byEmod totalMonths 12 (by decide) |>.add 1
+  let yearsOffset := totalMonths / 12
+  PlainDate.ofYearMonthDayClip (date.year.add yearsOffset) wrappedMonths date.day
+
+/--
+Subtracts `Month.Offset` from a `PlainDate`, it clips the day to the last valid day of that month.
+-/
+@[inline]
+def subMonthsClip (date : PlainDate) (months : Month.Offset) : PlainDate :=
+  addMonthsClip date (-months)
+
+/--
+Creates a `PlainDate` by rolling over the extra days to the next month.
+-/
+def rollOver (year : Year.Offset) (month : Month.Ordinal) (day : Day.Ordinal) : PlainDate :=
+  ofYearMonthDayClip year month 1 |>.addDays (day.toOffset - 1)
+
+/--
+Creates a new `PlainDate` by adjusting the year to the given `year` value. The month and day remain unchanged,
+and any invalid days for the new year will be handled according to the `clip` behavior.
+-/
+@[inline]
+def withYearClip (dt : PlainDate) (year : Year.Offset) : PlainDate :=
+  ofYearMonthDayClip year dt.month dt.day
+
+/--
+Creates a new `PlainDate` by adjusting the year to the given `year` value. The month and day are rolled
+over to the next valid month and day if necessary.
+-/
+@[inline]
+def withYearRollOver (dt : PlainDate) (year : Year.Offset) : PlainDate :=
+  rollOver year dt.month dt.day
+
+/--
+Adds a given number of months to a `PlainDate`, rolling over any excess days into the following month.
+-/
+def addMonthsRollOver (date : PlainDate) (months : Month.Offset) : PlainDate :=
+  addMonthsClip (ofYearMonthDayClip date.year date.month 1) months
+  |>.addDays (date.day.toOffset - 1)
+
+/--
+Subtracts `Month.Offset` from a `PlainDate`, rolling over excess days as needed.
+-/
+@[inline]
+def subMonthsRollOver (date : PlainDate) (months : Month.Offset) : PlainDate :=
+  addMonthsRollOver date (-months)
+
+/--
+Adds `Year.Offset` to a `PlainDate`, rolling over excess days to the next month, or next year.
+-/
+@[inline]
+def addYearsRollOver (date : PlainDate) (years : Year.Offset) : PlainDate :=
+  addMonthsRollOver date (years.mul 12)
+
+/--
+Subtracts `Year.Offset` from a `PlainDate`, rolling over excess days to the next month.
+-/
+@[inline]
+def subYearsRollOver (date : PlainDate) (years : Year.Offset) : PlainDate :=
+  addMonthsRollOver date (- years.mul 12)
+
+/--
+Adds `Year.Offset` to a `PlainDate`, clipping the day to the last valid day of the month.
+-/
+@[inline]
+def addYearsClip (date : PlainDate) (years : Year.Offset) : PlainDate :=
+  addMonthsClip date (years.mul 12)
+
+/--
+Subtracts `Year.Offset` from a `PlainDate`, clipping the day to the last valid day of the month.
+-/
+@[inline]
+def subYearsClip (date : PlainDate) (years : Year.Offset) : PlainDate :=
+  addMonthsClip date (- years.mul 12)
+
+/--
+Creates a new `PlainDate` by adjusting the day of the month to the given `days` value, with any
+out-of-range days clipped to the nearest valid date.
+-/
+@[inline]
+def withDaysClip (dt : PlainDate) (days : Day.Ordinal) : PlainDate :=
+  ofYearMonthDayClip dt.year dt.month days
+
+/--
+Creates a new `PlainDate` by adjusting the day of the month to the given `days` value, with any
+out-of-range days rolled over to the next month or year as needed.
+-/
+@[inline]
+def withDaysRollOver (dt : PlainDate) (days : Day.Ordinal) : PlainDate :=
+  rollOver dt.year dt.month days
+
+/--
+Creates a new `PlainDate` by adjusting the month to the given `month` value.
+The day remains unchanged, and any invalid days for the new month will be handled according to the `clip` behavior.
+-/
+@[inline]
+def withMonthClip (dt : PlainDate) (month : Month.Ordinal) : PlainDate :=
+  ofYearMonthDayClip dt.year month dt.day
+
+/--
+Creates a new `PlainDate` by adjusting the month to the given `month` value.
+The day is rolled over to the next valid month if necessary.
+-/
+@[inline]
+def withMonthRollOver (dt : PlainDate) (month : Month.Ordinal) : PlainDate :=
+  rollOver dt.year month dt.day
+
+/--
+Calculates the `Weekday` of a given `PlainDate` using Zeller's Congruence for the Gregorian calendar.
+-/
+def weekday (date : PlainDate) : Weekday :=
+  let days := date.toDaysSinceUNIXEpoch.val
+  let res := if days ≥ -4 then (days + 4) % 7 else (days + 5) % 7 + 6
+  .ofOrdinal (Bounded.LE.ofNatWrapping res (by decide))
+
+/--
+Determines the week of the month for the given `PlainDate`. The week of the month is calculated based
+on the day of the month and the weekday. Each week starts on Monday because the entire library is
+based on the Gregorian Calendar.
+-/
+def alignedWeekOfMonth (date : PlainDate) : Week.Ordinal.OfMonth :=
+  let weekday := date.withDaysClip 1 |>.weekday |>.toOrdinal |>.sub 1
+  let days := date.day |>.sub 1 |>.addBounds weekday
+  days |>.ediv 7 (by decide) |>.add 1
+
+/--
+Sets the date to the specified `desiredWeekday`. If the `desiredWeekday` is the same as the current weekday,
+the original `date` is returned without modification. If the `desiredWeekday` is in the future, the
+function adjusts the date forward to the next occurrence of that weekday.
+-/
+def withWeekday (date : PlainDate) (desiredWeekday : Weekday) : PlainDate :=
+  let weekday := date |>.weekday |>.toOrdinal
+  let offset := desiredWeekday.toOrdinal |>.subBounds weekday
+
+  let offset : Bounded.LE 0 6 :=
+    if h : offset.val < 0 then
+      offset.truncateTop (Int.le_sub_one_of_lt h) |>.addBounds (.exact 7)
+      |>.expandBottom (by decide)
+    else
+      offset.truncateBottom (Int.not_lt.mp h)
+      |>.expandTop (by decide)
+
+  date.addDays (Day.Offset.ofInt offset.toInt)
+
+/--
+Calculates the week of the year starting Monday for a given year.
+-/
+def weekOfYear (date : PlainDate) : Week.Ordinal :=
+  let y := date.year
+
+  let w := Bounded.LE.exact 10
+    |>.addBounds date.dayOfYear
+    |>.subBounds date.weekday.toOrdinal
+    |>.ediv 7 (by decide)
+
+  if h : w.val < 1 then
+    (y-1).weeks |>.expandBottom (by decide)
+  else if h₁ : w.val > y.weeks.val then
+    .ofNat' 1 (by decide)
+  else
+    let h := Int.not_lt.mp h
+    let h₁ := Int.not_lt.mp h₁
+    let w := w.truncateBottom h |>.truncateTop (Int.le_trans h₁ y.weeks.property.right)
+    w
+
+instance : HAdd PlainDate Day.Offset PlainDate where
+  hAdd := addDays
+
+instance : HSub PlainDate Day.Offset PlainDate where
+  hSub := subDays
+
+instance : HAdd PlainDate Week.Offset PlainDate where
+  hAdd := addWeeks
+
+instance : HSub PlainDate Week.Offset PlainDate where
+  hSub := subWeeks
+
+end PlainDate
+end Time
+end Std

src/Std/Time/Date/Unit/Basic.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Std.Time.Date.Unit.Day
+import Std.Time.Date.Unit.Month
+import Std.Time.Date.Unit.Year
+import Std.Time.Date.Unit.Weekday
+import Std.Time.Date.Unit.Week
+
+/-!
+This module defines various units used for measuring, counting, and converting between days, months,
+years, weekdays, and weeks of the year.
+
+The units are organized into types representing these time-related concepts, with operations provided
+to facilitate conversions and manipulations between them.
+-/
+
+namespace Std
+namespace Time
+open Internal
+
+namespace Day.Offset
+
+/--
+Convert `Week.Offset` into `Day.Offset`.
+-/
+@[inline]
+def ofWeeks (week : Week.Offset) : Day.Offset :=
+  week.mul 7
+
+/--
+Convert `Day.Offset` into `Week.Offset`.
+-/
+@[inline]
+def toWeeks (day : Day.Offset) : Week.Offset :=
+  day.ediv 7
+
+end Day.Offset

src/Std/Time/Date/Unit/Day.lean

@@ -0,0 +1,221 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Std.Time.Time
+
+namespace Std
+namespace Time
+namespace Day
+open Lean Internal
+
+set_option linter.all true
+
+/--
+`Ordinal` represents a bounded value for days, which ranges between 1 and 31.
+-/
+def Ordinal := Bounded.LE 1 31
+  deriving Repr, BEq, LE, LT
+
+instance : OfNat Ordinal n :=
+  inferInstanceAs (OfNat (Bounded.LE 1 (1 + (30 : Nat))) n)
+
+instance {x y : Ordinal} : Decidable (x ≤ y) :=
+  inferInstanceAs (Decidable (x.val ≤ y.val))
+
+instance {x y : Ordinal} : Decidable (x < y) :=
+  inferInstanceAs (Decidable (x.val < y.val))
+
+instance : Inhabited Ordinal where default := 1
+
+/--
+`Offset` represents an offset in days. It is defined as an `Int` with a base unit of 86400
+(the number of seconds in a day).
+-/
+def Offset : Type := UnitVal 86400
+  deriving Repr, BEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
+
+instance : OfNat Offset n := ⟨UnitVal.ofNat n⟩
+
+instance {x y : Offset} : Decidable (x ≤ y) :=
+  inferInstanceAs (Decidable (x.val ≤ y.val))
+
+instance {x y : Offset} : Decidable (x < y) :=
+  inferInstanceAs (Decidable (x.val < y.val))
+
+namespace Ordinal
+
+/--
+Creates an `Ordinal` from an integer, ensuring the value is within bounds.
+-/
+@[inline]
+def ofInt (data : Int) (h : 1 ≤ data ∧ data ≤ 31) : Ordinal :=
+  Bounded.LE.mk data h
+
+/--
+`OfYear` represents the day ordinal within a year, which can be bounded between 1 and 365 or 366,
+depending on whether it's a leap year.
+-/
+def OfYear (leap : Bool) := Bounded.LE 1 (.ofNat (if leap then 366 else 365))
+
+instance : Repr (OfYear leap) where
+  reprPrec r p := reprPrec r.val p
+
+instance : ToString (OfYear leap) where
+  toString r := toString r.val
+
+namespace OfYear
+
+/--
+Creates an ordinal for a specific day within the year, ensuring that the provided day (`data`)
+is within the valid range for the year, which can be 1 to 365 or 366 for leap years.
+-/
+@[inline]
+def ofNat (data : Nat) (h : data ≥ 1 ∧ data ≤ (if leap then 366 else 365) := by decide) : OfYear leap :=
+  Bounded.LE.ofNat' data h
+
+end OfYear
+
+instance : OfNat (Ordinal.OfYear leap) n :=
+  match leap with
+  | true => inferInstanceAs (OfNat (Bounded.LE 1 (1 + (365 : Nat))) n)
+  | false => inferInstanceAs (OfNat (Bounded.LE 1 (1 + (364 : Nat))) n)
+
+instance : Inhabited (Ordinal.OfYear leap) where
+  default := by
+    refine ⟨1, And.intro (by decide) ?_⟩
+    split <;> simp
+
+/--
+Creates an ordinal from a natural number, ensuring the number is within the valid range
+for days of a month (1 to 31).
+-/
+@[inline]
+def ofNat (data : Nat) (h : data ≥ 1 ∧ data ≤ 31 := by decide) : Ordinal :=
+  Bounded.LE.ofNat' data h
+
+/--
+Creates an ordinal from a `Fin` value, ensuring it is within the valid range for days of the month (1 to 31).
+If the `Fin` value is 0, it is converted to 1.
+-/
+@[inline]
+def ofFin (data : Fin 32) : Ordinal :=
+  Bounded.LE.ofFin' data (by decide)
+
+/--
+Converts an `Ordinal` to an `Offset`.
+-/
+@[inline]
+def toOffset (ordinal : Ordinal) : Offset :=
+  UnitVal.ofInt ordinal.val
+
+namespace OfYear
+
+/--
+Converts an `OfYear` ordinal to a `Offset`.
+-/
+def toOffset (ofYear : OfYear leap) : Offset :=
+  UnitVal.ofInt ofYear.val
+
+end OfYear
+end Ordinal
+
+namespace Offset
+
+/--
+Converts an `Offset` to an `Ordinal`.
+-/
+@[inline]
+def toOrdinal (off : Day.Offset) (h : off.val ≥ 1 ∧ off.val ≤ 31) : Ordinal :=
+  Bounded.LE.mk off.val h
+
+/--
+Creates an `Offset` from a natural number.
+-/
+@[inline]
+def ofNat (data : Nat) : Day.Offset :=
+  UnitVal.ofInt data
+
+/--
+Creates an `Offset` from an integer.
+-/
+@[inline]
+def ofInt (data : Int) : Day.Offset :=
+  UnitVal.ofInt data
+
+/--
+Convert `Day.Offset` into `Nanosecond.Offset`.
+-/
+@[inline]
+def toNanoseconds (days : Day.Offset) : Nanosecond.Offset :=
+  days.mul 86400000000000
+
+/--
+Convert `Nanosecond.Offset` into `Day.Offset`.
+-/
+@[inline]
+def ofNanoseconds (ns : Nanosecond.Offset) : Day.Offset :=
+  ns.ediv 86400000000000
+
+/--
+Convert `Day.Offset` into `Millisecond.Offset`.
+-/
+@[inline]
+def toMilliseconds (days : Day.Offset) : Millisecond.Offset :=
+  days.mul 86400000
+
+/--
+Convert `Millisecond.Offset` into `Day.Offset`.
+-/
+@[inline]
+def ofMilliseconds (ms : Millisecond.Offset) : Day.Offset :=
+  ms.ediv 86400000
+
+/--
+Convert `Day.Offset` into `Second.Offset`.
+-/
+@[inline]
+def toSeconds (days : Day.Offset) : Second.Offset :=
+  days.mul 86400
+
+/--
+Convert `Second.Offset` into `Day.Offset`.
+-/
+@[inline]
+def ofSeconds (secs : Second.Offset) : Day.Offset :=
+  secs.ediv 86400
+
+/--
+Convert `Day.Offset` into `Minute.Offset`.
+-/
+@[inline]
+def toMinutes (days : Day.Offset) : Minute.Offset :=
+  days.mul 1440
+
+/--
+Convert `Minute.Offset` into `Day.Offset`.
+-/
+@[inline]
+def ofMinutes (minutes : Minute.Offset) : Day.Offset :=
+  minutes.ediv 1440
+
+/--
+Convert `Day.Offset` into `Hour.Offset`.
+-/
+@[inline]
+def toHours (days : Day.Offset) : Hour.Offset :=
+  days.mul 24
+
+/--
+Convert `Hour.Offset` into `Day.Offset`.
+-/
+@[inline]
+def ofHours (hours : Hour.Offset) : Day.Offset :=
+  hours.ediv 24
+
+end Offset
+end Day
+end Time
+end Std

src/Std/Time/Date/Unit/Month.lean

@@ -0,0 +1,308 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Std.Internal.Rat
+import Std.Time.Date.Unit.Day
+
+namespace Std
+namespace Time
+namespace Month
+open Std.Internal
+open Internal
+
+set_option linter.all true
+
+/--
+`Ordinal` represents a bounded value for months, which ranges between 1 and 12.
+-/
+def Ordinal := Bounded.LE 1 12
+  deriving Repr, BEq, LE, LT
+
+instance : OfNat Ordinal n :=
+  inferInstanceAs (OfNat (Bounded.LE 1 (1 + (11 : Nat))) n)
+
+instance : Inhabited Ordinal where
+  default := 1
+
+instance {x y : Ordinal} : Decidable (x ≤ y) :=
+  inferInstanceAs (Decidable (x.val ≤ y.val))
+
+instance {x y : Ordinal} : Decidable (x < y) :=
+  inferInstanceAs (Decidable (x.val < y.val))
+
+/--
+`Offset` represents an offset in months. It is defined as an `Int`.
+-/
+def Offset : Type := Int
+  deriving Repr, BEq, Inhabited, Add, Sub, Mul, Div, Neg, ToString, LT, LE, DecidableEq
+
+instance : OfNat Offset n :=
+  ⟨Int.ofNat n⟩
+
+/--
+`Quarter` represents a value between 1 and 4, inclusive, corresponding to the four quarters of a year.
+-/
+def Quarter := Bounded.LE 1 4
+
+namespace Quarter
+
+/--
+Determine the `Quarter` by the month.
+-/
+def ofMonth (month : Month.Ordinal) : Quarter :=
+  month
+  |>.sub 1
+  |>.ediv 3 (by decide)
+  |>.add 1
+
+end Quarter
+
+namespace Offset
+
+/--
+Creates an `Offset` from a natural number.
+-/
+@[inline]
+def ofNat (data : Nat) : Offset :=
+  .ofNat data
+
+/--
+Creates an `Offset` from an integer.
+-/
+@[inline]
+def ofInt (data : Int) : Offset :=
+  data
+
+end Offset
+
+namespace Ordinal
+
+/--
+The ordinal value representing the month of January.
+-/
+@[inline] def january : Ordinal := 1
+
+/--
+The ordinal value representing the month of February.
+-/
+@[inline] def february : Ordinal := 2
+
+/--
+The ordinal value representing the month of March.
+-/
+@[inline] def march : Ordinal := 3
+
+/--
+The ordinal value representing the month of April.
+-/
+@[inline] def april : Ordinal := 4
+
+/--
+The ordinal value representing the month of May.
+-/
+@[inline] def may : Ordinal := 5
+
+/--
+The ordinal value representing the month of June.
+-/
+@[inline] def june : Ordinal := 6
+
+/--
+The ordinal value representing the month of July.
+-/
+@[inline] def july : Ordinal := 7
+
+/--
+The ordinal value representing the month of August.
+-/
+@[inline] def august : Ordinal := 8
+
+/--
+The ordinal value representing the month of September.
+-/
+@[inline] def september : Ordinal := 9
+
+/--
+The ordinal value representing the month of October.
+-/
+@[inline] def october : Ordinal := 10
+
+/--
+The ordinal value representing the month of November.
+-/
+@[inline] def november : Ordinal := 11
+
+/--
+The ordinal value representing the month of December.
+-/
+@[inline] def december : Ordinal := 12
+
+/--
+Converts a `Ordinal` into a `Offset`.
+-/
+@[inline]
+def toOffset (month : Ordinal) : Offset :=
+  month.val
+
+/--
+Creates an `Ordinal` from an integer, ensuring the value is within bounds.
+-/
+@[inline]
+def ofInt (data : Int) (h : 1 ≤ data ∧ data ≤ 12) : Ordinal :=
+  Bounded.LE.mk data h
+
+/--
+Creates an `Ordinal` from a `Nat`, ensuring the value is within bounds.
+-/
+@[inline]
+def ofNat (data : Nat) (h : data ≥ 1 ∧ data ≤ 12 := by decide) : Ordinal :=
+  Bounded.LE.ofNat' data h
+
+/--
+Converts a `Ordinal` into a `Nat`.
+-/
+@[inline]
+def toNat (month : Ordinal) : Nat := by
+  match month with
+  | ⟨.ofNat s, _⟩ => exact s
+  | ⟨.negSucc s, h⟩ => nomatch h.left
+
+/--
+Creates an `Ordinal` from a `Fin`, ensuring the value is within bounds, if its 0 then its converted
+to 1.
+-/
+@[inline]
+def ofFin (data : Fin 13) : Ordinal :=
+  Bounded.LE.ofFin' data (by decide)
+
+/--
+Transforms `Month.Ordinal` into `Second.Offset`.
+-/
+def toSeconds (leap : Bool) (month : Ordinal) : Second.Offset :=
+  let daysAcc := #[0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334]
+  let days : Day.Offset := daysAcc[month.toNat]!
+  let time := days.toSeconds
+  if leap && month.toNat ≥ 2
+    then time + 86400
+    else time
+
+/--
+Transforms `Month.Ordinal` into `Minute.Offset`.
+-/
+@[inline]
+def toMinutes (leap : Bool) (month : Ordinal) : Minute.Offset :=
+  toSeconds leap month
+  |>.ediv 60
+
+/--
+Transforms `Month.Ordinal` into `Hour.Offset`.
+-/
+@[inline]
+def toHours (leap : Bool) (month : Ordinal) : Hour.Offset :=
+  toMinutes leap month
+  |>.ediv 60
+
+/--
+Transforms `Month.Ordinal` into `Day.Offset`.
+-/
+@[inline]
+def toDays (leap : Bool) (month : Ordinal) : Day.Offset :=
+  toSeconds leap month
+  |>.convert
+
+/--
+Size in days of each month if the year is not a leap year.
+-/
+@[inline]
+private def monthSizesNonLeap : { val : Array Day.Ordinal // val.size = 12 } :=
+  ⟨#[31, 28, 31, 30, 31, 30, 31, 31, 30, 31, 30, 31], by decide⟩
+
+/--
+Returns the cumulative size in days of each month for a non-leap year.
+-/
+@[inline]
+private def cumulativeSizes : { val : Array Day.Offset // val.size = 12 } :=
+  ⟨#[0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334], by decide⟩
+
+/--
+Gets the number of days in a month.
+-/
+def days (leap : Bool) (month : Ordinal) : Day.Ordinal :=
+  if month.val = 2 then
+    if leap then 29 else 28
+  else
+    let ⟨months, p⟩ := monthSizesNonLeap
+    let index : Fin 12 := (month.sub 1).toFin (by decide)
+    let idx := (index.cast (by rw [p]))
+    months.get idx.val idx.isLt
+
+theorem days_gt_27 (leap : Bool) (i : Month.Ordinal) : days leap i > 27 := by
+  match i with
+  | ⟨2, _⟩ =>
+    simp [days]
+    split <;> decide
+  | ⟨1, _⟩ | ⟨3, _⟩ | ⟨4, _⟩ | ⟨5, _⟩ | ⟨6, _⟩ | ⟨7, _⟩
+  | ⟨8, _⟩ | ⟨9, _⟩ | ⟨10, _⟩ | ⟨11, _⟩ | ⟨12, _⟩ =>
+    simp [days, monthSizesNonLeap]
+    decide +revert
+
+/--
+Returns the number of days until the `month`.
+-/
+def cumulativeDays (leap : Bool) (month : Ordinal) : Day.Offset := by
+  let ⟨months, p⟩ := cumulativeSizes
+  let index : Fin 12 := (month.sub 1).toFin (by decide)
+  rw [← p] at index
+  let res := months.get index.val index.isLt
+  exact res + (if leap ∧ month.val > 2 then 1 else 0)
+
+theorem cumulativeDays_le (leap : Bool) (month : Month.Ordinal) : cumulativeDays leap month ≥ 0 ∧ cumulativeDays leap month ≤ 334 + (if leap then 1 else 0) := by
+  match month with
+  | ⟨1, _⟩ | ⟨2, _⟩ | ⟨3, _⟩  | ⟨4, _⟩  | ⟨5, _⟩  | ⟨6, _⟩  | ⟨7, _⟩  | ⟨8, _⟩  | ⟨9, _⟩  | ⟨10, _⟩  | ⟨11, _⟩ | ⟨12, _⟩ =>
+    simp [cumulativeSizes, Bounded.LE.sub, Bounded.LE.add, Bounded.LE.toFin, cumulativeDays]
+    try split
+    all_goals decide +revert
+
+theorem difference_eq (p : month.val ≤ 11) :
+  let next := month.truncateTop p |>.addTop 1 (by decide)
+  (cumulativeDays leap next).val = (cumulativeDays leap month).val + (days leap month).val := by
+  match month with
+  | ⟨1, _⟩ | ⟨2, _⟩ | ⟨3, _⟩  | ⟨4, _⟩  | ⟨5, _⟩  | ⟨6, _⟩  | ⟨7, _⟩  | ⟨8, _⟩  | ⟨9, _⟩  | ⟨10, _⟩  | ⟨11, _⟩ =>
+    simp [cumulativeDays, Bounded.LE.addTop, days, monthSizesNonLeap];
+    try split <;> rfl
+    try rfl
+  | ⟨12, _⟩ => contradiction
+
+/--
+Checks if a given day is valid for the specified month and year. For example, `29/02` is valid only
+if the year is a leap year.
+-/
+abbrev Valid (leap : Bool) (month : Month.Ordinal) (day : Day.Ordinal) : Prop :=
+  day.val ≤ (days leap month).val
+
+/--
+Clips the day to be within the valid range.
+-/
+@[inline]
+def clipDay (leap : Bool) (month : Month.Ordinal) (day : Day.Ordinal) : Day.Ordinal :=
+  let max : Day.Ordinal := month.days leap
+  if day.val > max.val
+    then max
+    else day
+
+/--
+Proves that every value provided by a clipDay is a valid day in a year.
+-/
+theorem valid_clipDay : Valid leap month (clipDay leap month day) := by
+  simp [Valid, clipDay]
+  split
+  exact Int.le_refl (days leap month).val
+  next h => exact Int.not_lt.mp h
+
+end Ordinal
+end Month
+end Time
+end Std

src/Std/Time/Date/Unit/Week.lean

@@ -0,0 +1,185 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Std.Internal.Rat
+import Std.Time.Date.Unit.Day
+
+namespace Std
+namespace Time
+namespace Week
+open Std.Internal
+open Internal
+
+set_option linter.all true
+
+/--
+`Ordinal` represents a bounded value for weeks, which ranges between 1 and 53.
+-/
+def Ordinal := Bounded.LE 1 53
+  deriving Repr, BEq, LE, LT
+
+instance : OfNat Ordinal n :=
+  inferInstanceAs (OfNat (Bounded.LE 1 (1 + (52 : Nat))) n)
+
+instance {x y : Ordinal} : Decidable (x ≤ y) :=
+  inferInstanceAs (Decidable (x.val ≤ y.val))
+
+instance {x y : Ordinal} : Decidable (x < y) :=
+  inferInstanceAs (Decidable (x.val < y.val))
+
+instance : Inhabited Ordinal where
+  default := 1
+
+/--
+`Offset` represents an offset in weeks.
+-/
+def Offset : Type := UnitVal (86400 * 7)
+  deriving Repr, BEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
+
+instance : OfNat Offset n := ⟨UnitVal.ofNat n⟩
+
+namespace Ordinal
+
+/--
+Creates an `Ordinal` from an integer, ensuring the value is within bounds.
+-/
+@[inline]
+def ofInt (data : Int) (h : 1 ≤ data ∧ data ≤ 53) : Ordinal :=
+  Bounded.LE.mk data h
+
+/--
+`OfMonth` represents the number of weeks within a month. It ensures that the week is within the
+correct bounds—either 1 to 6, representing the possible weeks in a month.
+-/
+def OfMonth := Bounded.LE 1 6
+  deriving Repr
+
+/--
+Creates an `Ordinal` from a natural number, ensuring the value is within bounds.
+-/
+@[inline]
+def ofNat (data : Nat) (h : data ≥ 1 ∧ data ≤ 53 := by decide) : Ordinal :=
+  Bounded.LE.ofNat' data h
+
+/--
+Creates an `Ordinal` from a `Fin`, ensuring the value is within bounds.
+-/
+@[inline]
+def ofFin (data : Fin 54) : Ordinal :=
+  Bounded.LE.ofFin' data (by decide)
+
+/--
+Converts an `Ordinal` to an `Offset`.
+-/
+@[inline]
+def toOffset (ordinal : Ordinal) : Offset :=
+  UnitVal.ofInt ordinal.val
+
+end Ordinal
+namespace Offset
+
+/--
+Creates an `Offset` from a natural number.
+-/
+@[inline]
+def ofNat (data : Nat) : Week.Offset :=
+  UnitVal.ofInt data
+
+/--
+Creates an `Offset` from an integer.
+-/
+@[inline]
+def ofInt (data : Int) : Week.Offset :=
+  UnitVal.ofInt data
+
+/--
+Convert `Week.Offset` into `Millisecond.Offset`.
+-/
+@[inline]
+def toMilliseconds (weeks : Week.Offset) : Millisecond.Offset :=
+  weeks.mul 604800000
+
+/--
+Convert `Millisecond.Offset` into `Week.Offset`.
+-/
+@[inline]
+def ofMilliseconds (millis : Millisecond.Offset) : Week.Offset :=
+  millis.ediv 604800000
+
+/--
+Convert `Week.Offset` into `Nanosecond.Offset`.
+-/
+@[inline]
+def toNanoseconds (weeks : Week.Offset) : Nanosecond.Offset :=
+  weeks.mul 604800000000000
+
+/--
+Convert `Nanosecond.Offset` into `Week.Offset`.
+-/
+@[inline]
+def ofNanoseconds (nanos : Nanosecond.Offset) : Week.Offset :=
+  nanos.ediv 604800000000000
+
+/--
+Convert `Week.Offset` into `Second.Offset`.
+-/
+@[inline]
+def toSeconds (weeks : Week.Offset) : Second.Offset :=
+  weeks.mul 604800
+
+/--
+Convert `Second.Offset` into `Week.Offset`.
+-/
+@[inline]
+def ofSeconds (secs : Second.Offset) : Week.Offset :=
+  secs.ediv 604800
+
+/--
+Convert `Week.Offset` into `Minute.Offset`.
+-/
+@[inline]
+def toMinutes (weeks : Week.Offset) : Minute.Offset :=
+  weeks.mul 10080
+
+/--
+Convert `Minute.Offset` into `Week.Offset`.
+-/
+@[inline]
+def ofMinutes (minutes : Minute.Offset) : Week.Offset :=
+  minutes.ediv 10080
+
+/--
+Convert `Week.Offset` into `Hour.Offset`.
+-/
+@[inline]
+def toHours (weeks : Week.Offset) : Hour.Offset :=
+  weeks.mul 168
+
+/--
+Convert `Hour.Offset` into `Week.Offset`.
+-/
+@[inline]
+def ofHours (hours : Hour.Offset) : Week.Offset :=
+  hours.ediv 168
+
+/--
+Convert `Week.Offset` into `Day.Offset`.
+-/
+@[inline]
+def toDays (weeks : Week.Offset) : Day.Offset :=
+  weeks.mul 7
+
+/--
+Convert `Day.Offset` into `Week.Offset`.
+-/
+@[inline]
+def ofDays (days : Day.Offset) : Week.Offset :=
+  days.ediv 7
+
+end Offset
+end Week
+end Time
+end Std

src/Std/Time/Date/Unit/Weekday.lean

@@ -0,0 +1,134 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Std.Internal.Rat
+import Std.Time.Date.Unit.Day
+
+namespace Std
+namespace Time
+open Std.Internal
+open Internal
+
+set_option linter.all true
+
+/--
+Defines the enumeration for days of the week. Each variant corresponds to a day of the week.
+-/
+inductive Weekday
+  /-- Monday. -/
+  | monday
+
+  /-- Tuesday. -/
+  | tuesday
+
+  /-- Wednesday. -/
+  | wednesday
+
+  /-- Thursday. -/
+  | thursday
+
+  /-- Friday. -/
+  | friday
+
+  /-- Saturday. -/
+  | saturday
+
+    /-- Sunday. -/
+  | sunday
+  deriving Repr, Inhabited, BEq
+
+namespace Weekday
+
+/--
+`Ordinal` represents a bounded value for weekdays, which ranges between 1 and 7.
+-/
+def Ordinal := Bounded.LE 1 7
+
+instance : OfNat Ordinal n :=
+  inferInstanceAs (OfNat (Bounded.LE 1 (1 + (6 : Nat))) n)
+
+/--
+Converts a `Ordinal` representing a day index into a corresponding `Weekday`. This function is useful
+for mapping numerical representations to days of the week.
+-/
+def ofOrdinal : Ordinal → Weekday
+  | 1 => .monday
+  | 2 => .tuesday
+  | 3 => .wednesday
+  | 4 => .thursday
+  | 5 => .friday
+  | 6 => .saturday
+  | 7 => .sunday
+
+/--
+Converts a `Weekday` to a `Ordinal`.
+-/
+def toOrdinal : Weekday → Ordinal
+  | .monday => 1
+  | .tuesday => 2
+  | .wednesday => 3
+  | .thursday => 4
+  | .friday => 5
+  | .saturday => 6
+  | .sunday => 7
+
+/--
+Converts a `Weekday` to a `Nat`.
+-/
+def toNat : Weekday → Nat
+  | .monday => 1
+  | .tuesday => 2
+  | .wednesday => 3
+  | .thursday => 4
+  | .friday => 5
+  | .saturday => 6
+  | .sunday => 7
+
+/--
+Converts a `Nat` to an `Option Weekday`.
+-/
+def ofNat? : Nat → Option Weekday
+  | 1 => some .monday
+  | 2 => some .tuesday
+  | 3 => some .wednesday
+  | 4 => some .thursday
+  | 5 => some .friday
+  | 6 => some .saturday
+  | 7 => some .sunday
+  | _ => none
+
+/--
+Converts a `Nat` to a `Weekday`. Panics if the value provided is invalid.
+-/
+@[inline]
+def ofNat! (n : Nat) : Weekday :=
+  match ofNat? n with
+  | some res => res
+  | none => panic! "invalid weekday"
+
+/--
+Gets the next `Weekday`.
+-/
+def next : Weekday → Weekday
+  | .monday => .tuesday
+  | .tuesday => .wednesday
+  | .wednesday => .thursday
+  | .thursday => .friday
+  | .friday => .saturday
+  | .saturday => .sunday
+  | .sunday => .monday
+
+/--
+Check if it's a weekend.
+-/
+def isWeekend : Weekday → Bool
+  | .saturday => true
+  | .sunday => true
+  | _ => false
+
+end Weekday
+end Time
+end Std

src/Std/Time/Date/Unit/Year.lean

@@ -0,0 +1,128 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Std.Time.Internal
+import Std.Internal.Rat
+import Std.Time.Date.Unit.Day
+import Std.Time.Date.Unit.Month
+
+namespace Std
+namespace Time
+namespace Year
+open Std.Internal
+open Internal
+
+set_option linter.all true
+
+/--
+Defines the different eras.
+-/
+inductive Era
+  /-- The era before the Common Era (BCE), always represents a date before year 0. -/
+  | bce
+
+  /-- The Common Era (CE), represents dates from year 0 onwards. -/
+  | ce
+  deriving Repr, Inhabited
+
+instance : ToString Era where
+  toString
+    | .bce => "BCE"
+    | .ce => "CE"
+
+/--
+`Offset` represents a year offset, defined as an `Int`.
+-/
+def Offset : Type := Int
+  deriving Repr, BEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
+
+instance {x y : Offset} : Decidable (x ≤ y) :=
+  let x : Int := x
+  inferInstanceAs (Decidable (x ≤ y))
+
+instance {x y : Offset} : Decidable (x < y) :=
+  let x : Int := x
+  inferInstanceAs (Decidable (x < y))
+
+instance : OfNat Offset n := ⟨Int.ofNat n⟩
+
+namespace Offset
+
+/--
+Creates an `Offset` from a natural number.
+-/
+@[inline]
+def ofNat (data : Nat) : Offset :=
+  .ofNat data
+
+/--
+Creates an `Offset` from an integer.
+-/
+@[inline]
+def ofInt (data : Int) : Offset :=
+  data
+
+/--
+Converts the `Year` offset to an `Int`.
+-/
+@[inline]
+def toInt (offset : Offset) : Int :=
+  offset
+
+/--
+Converts the `Year` offset to a `Month` offset.
+-/
+@[inline]
+def toMonths (val : Offset) : Month.Offset :=
+  val.mul 12
+
+/--
+Determines if a year is a leap year in the proleptic Gregorian calendar.
+-/
+@[inline]
+def isLeap (y : Offset) : Bool :=
+  y.toInt.tmod 4 = 0 ∧ (y.toInt.tmod 100 ≠ 0 ∨ y.toInt.tmod 400 = 0)
+
+/--
+Returns the `Era` of the `Year`.
+-/
+def era (year : Offset) : Era :=
+  if year.toInt ≥ 1
+    then .ce
+    else .bce
+
+/--
+Calculates the number of days in the specified `year`.
+-/
+def days (year : Offset) : Bounded.LE 365 366 :=
+  if year.isLeap
+    then .ofNatWrapping 366 (by decide)
+    else .ofNatWrapping 355 (by decide)
+
+/--
+Calculates the number of weeks in the specified `year`.
+-/
+def weeks (year : Offset) : Bounded.LE 52 53 :=
+  let p (year : Offset) := Bounded.LE.byEmod (year.toInt + year.toInt/4 - year.toInt/100 + year.toInt/400) 7 (by decide)
+
+  let add : Bounded.LE 0 1 :=
+    if (p year).val = 4 ∨ (p (year - 1)).val = 3
+      then Bounded.LE.ofNat 1 (by decide)
+      else Bounded.LE.ofNat 0 (by decide)
+
+  Bounded.LE.exact 52 |>.addBounds add
+
+/--
+Checks if the given date is valid for the specified year, month, and day.
+-/
+@[inline]
+abbrev Valid (year : Year.Offset) (month : Month.Ordinal) (day : Day.Ordinal) : Prop :=
+  day ≤ month.days year.isLeap
+
+end Offset
+end Year
+end Time
+end Std

src/Std/Time/Date/ValidDate.lean

@@ -0,0 +1,88 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Std.Internal.Rat
+import Std.Time.Date.Unit.Day
+import Std.Time.Date.Unit.Month
+
+namespace Std
+namespace Time
+open Std.Internal
+open Internal
+open Month.Ordinal
+
+set_option linter.all true
+
+/--
+Represents a valid date for a given year, considering whether it is a leap year. Example: `(2, 29)`
+is valid only if `leap` is `true`.
+-/
+def ValidDate (leap : Bool) := { val : Month.Ordinal × Day.Ordinal // Valid leap (Prod.fst val) (Prod.snd val) }
+
+instance : Inhabited (ValidDate l) where
+  default := ⟨⟨1, 1⟩, (by cases l <;> decide)⟩
+
+namespace ValidDate
+
+/--
+Transforms a tuple of a `Month` and a `Day` into a `Day.Ordinal.OfYear`.
+-/
+def dayOfYear (ordinal : ValidDate leap) : Day.Ordinal.OfYear leap :=
+  let days := cumulativeDays leap ordinal.val.fst
+  let proof := cumulativeDays_le leap ordinal.val.fst
+  let bounded := Bounded.LE.mk days.toInt proof |>.addBounds ordinal.val.snd
+  match leap, bounded with
+  | true, bounded => bounded
+  | false, bounded => bounded
+
+/--
+Transforms a `Day.Ordinal.OfYear` into a tuple of a `Month` and a `Day`.
+-/
+def ofOrdinal (ordinal : Day.Ordinal.OfYear leap) : ValidDate leap :=
+    let rec go (idx : Month.Ordinal) (acc : Int) (h : ordinal.val > acc) (p : acc = (cumulativeDays leap idx).val) : ValidDate leap :=
+      let monthDays := days leap idx
+      if h₁ : ordinal.val ≤ acc + monthDays.val then
+        let bounded := Bounded.LE.mk ordinal.val (And.intro h h₁) |>.sub acc
+        let bounded : Bounded.LE 1 monthDays.val := bounded.cast (by omega) (by omega)
+        let days₁ : Day.Ordinal := ⟨bounded.val, And.intro bounded.property.left (Int.le_trans bounded.property.right monthDays.property.right)⟩
+        ⟨⟨idx, days₁⟩, Int.le_trans bounded.property.right (by simp)⟩
+      else by
+        let h₂ := Int.not_le.mp h₁
+
+        have h₃ : idx.val < 12 := Int.not_le.mp <| λh₃ => by
+          have h₅ := ordinal.property.right
+          let eq := Int.eq_iff_le_and_ge.mpr (And.intro idx.property.right h₃)
+          simp [monthDays, days, eq] at h₂
+          simp [cumulativeDays, eq] at p
+          simp [p] at h₂
+          cases leap
+          all_goals (simp at h₂; simp_all)
+          · have h₂ : 365 < ordinal.val := h₂
+            omega
+          · have h₂ : 366 < ordinal.val := h₂
+            omega
+
+        let idx₂ := idx.truncateTop (Int.le_sub_one_of_lt h₃) |>.addTop 1 (by decide)
+        refine go idx₂ (acc + monthDays.val) h₂ ?_
+        simp [monthDays, p]
+        rw [difference_eq (Int.le_of_lt_add_one h₃)]
+
+      termination_by 12 - idx.val.toNat
+      decreasing_by
+        simp_wf
+        simp [Bounded.LE.addTop]
+        let gt0 : idx.val ≥ 0 := Int.le_trans (by decide) idx.property.left
+        refine Nat.sub_lt_sub_left (Int.toNat_lt gt0 |>.mpr h₃) ?_
+        let toNat_lt_lt {n z : Int} (h : 0 ≤ z) (h₁ : 0 ≤ n) : z.toNat < n.toNat ↔ z < n := by
+          rw [← Int.not_le, ← Nat.not_le, ← Int.ofNat_le, Int.toNat_of_nonneg h, Int.toNat_of_nonneg h₁]
+        rw [toNat_lt_lt (by omega) (by omega)]
+        omega
+
+    go 1 0 (Int.le_trans (by decide) ordinal.property.left) (by cases leap <;> decide)
+
+end ValidDate
+end Time
+end Std

src/Std/Time/DateTime.lean

@@ -0,0 +1,104 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Std.Time.DateTime.Timestamp
+import Std.Time.DateTime.PlainDateTime
+
+namespace Std
+namespace Time
+
+namespace Timestamp
+
+set_option linter.all true
+
+/--
+Converts a `PlainDateTime` to a `Timestamp`
+-/
+@[inline]
+def ofPlainDateTimeAssumingUTC (pdt : PlainDateTime) : Timestamp :=
+  pdt.toTimestampAssumingUTC
+
+/--
+Converts a `Timestamp` to a `PlainDateTime`
+-/
+@[inline]
+def toPlainDateTimeAssumingUTC (timestamp : Timestamp) : PlainDateTime :=
+  PlainDateTime.ofTimestampAssumingUTC timestamp
+
+/--
+Converts a `PlainDate` to a `Timestamp`
+-/
+@[inline]
+def ofPlainDateAssumingUTC (pd : PlainDate) : Timestamp :=
+  let days := pd.toDaysSinceUNIXEpoch
+  let secs := days.toSeconds
+  Timestamp.ofSecondsSinceUnixEpoch secs
+
+/--
+Converts a `Timestamp` to a `PlainDate`
+-/
+@[inline]
+def toPlainDateAssumingUTC (timestamp : Timestamp) : PlainDate :=
+  let secs := timestamp.toSecondsSinceUnixEpoch
+  let days := Day.Offset.ofSeconds secs
+  PlainDate.ofDaysSinceUNIXEpoch days
+
+/--
+Converts a `Timestamp` to a `PlainTime`
+-/
+@[inline]
+def getTimeAssumingUTC (timestamp : Timestamp) : PlainTime :=
+  let nanos := timestamp.toNanosecondsSinceUnixEpoch
+  PlainTime.ofNanoseconds nanos
+
+end Timestamp
+namespace PlainDate
+
+/--
+Converts a `PlainDate` to a `Timestamp`
+-/
+@[inline]
+def toTimestampAssumingUTC (pdt : PlainDate) : Timestamp :=
+  Timestamp.ofPlainDateAssumingUTC pdt
+
+instance : HSub PlainDate PlainDate Duration where
+  hSub x y := x.toTimestampAssumingUTC - y.toTimestampAssumingUTC
+
+end PlainDate
+namespace PlainDateTime
+
+/--
+Converts a `PlainDate` to a `Timestamp`
+-/
+@[inline]
+def ofPlainDate (date : PlainDate) : PlainDateTime :=
+  { date, time := PlainTime.midnight }
+
+/--
+Converts a `PlainDateTime` to a `PlainDate`
+-/
+@[inline]
+def toPlainDate (pdt : PlainDateTime) : PlainDate :=
+  pdt.date
+
+/--
+Converts a `PlainTime` to a `PlainDateTime`
+-/
+@[inline]
+def ofPlainTime (time : PlainTime) : PlainDateTime :=
+  { date := ⟨1, 1, 1, by decide⟩, time }
+
+/--
+Converts a `PlainDateTime` to a `PlainTime`
+-/
+@[inline]
+def toPlainTime (pdt : PlainDateTime) : PlainTime :=
+  pdt.time
+
+instance : HSub PlainDateTime PlainDateTime Duration where
+  hSub x y := x.toTimestampAssumingUTC - y.toTimestampAssumingUTC
+
+end PlainDateTime

src/Std/Time/DateTime/PlainDateTime.lean

@@ -0,0 +1,601 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Std.Time.Date
+import Std.Time.Time
+import Std.Time.Internal
+import Std.Time.DateTime.Timestamp
+
+namespace Std
+namespace Time
+open Internal
+
+set_option linter.all true
+
+/--
+Represents a date and time with components for Year, Month, Day, Hour, Minute, Second, and Nanosecond.
+-/
+structure PlainDateTime where
+
+  /--
+  The `Date` component of a `PlainDate`
+  -/
+  date : PlainDate
+
+  /--
+  The `Time` component of a `PlainTime`
+  -/
+  time : PlainTime
+
+  deriving Inhabited, BEq, Repr
+
+namespace PlainDateTime
+
+/--
+Converts a `PlainDateTime` to a `Timestamp`
+-/
+def toTimestampAssumingUTC (dt : PlainDateTime) : Timestamp :=
+  let days := dt.date.toDaysSinceUNIXEpoch
+  let nanos := days.toSeconds + dt.time.toSeconds |>.mul 1000000000
+  let nanos := nanos.val + dt.time.nanosecond.val
+  Timestamp.ofNanosecondsSinceUnixEpoch (Nanosecond.Offset.ofInt nanos)
+
+/--
+Converts a `Timestamp` to a `PlainDateTime`.
+-/
+def ofTimestampAssumingUTC (stamp : Timestamp) : PlainDateTime := Id.run do
+  let leapYearEpoch := 11017
+  let daysPer400Y := 365 * 400 + 97
+  let daysPer100Y := 365 * 100 + 24
+  let daysPer4Y := 365 * 4 + 1
+
+  let nanos := stamp.toNanosecondsSinceUnixEpoch
+  let secs : Second.Offset := nanos.ediv 1000000000
+  let daysSinceEpoch : Day.Offset := secs.ediv 86400
+  let boundedDaysSinceEpoch := daysSinceEpoch
+
+  let mut rawDays := boundedDaysSinceEpoch - leapYearEpoch
+  let mut rem := Bounded.LE.byMod secs.val 86400 (by decide)
+
+  let ⟨remSecs, days⟩ :=
+    if h : rem.val ≤ -1 then
+      let remSecs := rem.truncateTop h
+      let remSecs : Bounded.LE 1 86399 := remSecs.add 86400
+      let rawDays := rawDays - 1
+      (remSecs.expandBottom (by decide), rawDays)
+    else
+      let h := rem.truncateBottom (Int.not_le.mp h)
+      (h, rawDays)
+
+  let mut quadracentennialCycles := days.val / daysPer400Y;
+  let mut remDays := days.val % daysPer400Y;
+
+  if remDays < 0 then
+    remDays := remDays + daysPer400Y
+    quadracentennialCycles := quadracentennialCycles - 1
+
+  let mut centenialCycles := remDays / daysPer100Y;
+
+  if centenialCycles = 4 then
+    centenialCycles := centenialCycles - 1
+
+  remDays := remDays - centenialCycles * daysPer100Y
+  let mut quadrennialCycles := remDays / daysPer4Y;
+
+  if quadrennialCycles = 25 then
+    quadrennialCycles := quadrennialCycles - 1
+
+  remDays := remDays - quadrennialCycles * daysPer4Y
+  let mut remYears := remDays / 365;
+
+  if remYears = 4 then
+    remYears := remYears - 1
+
+  remDays := remDays - remYears * 365
+
+  let mut year := 2000 + remYears + 4 * quadrennialCycles + 100 * centenialCycles + 400 * quadracentennialCycles
+  let months := [31, 30, 31, 30, 31, 31, 30, 31, 30, 31, 31, 29];
+  let mut mon : Fin 13 := 0;
+
+  for monLen in months do
+    mon := mon + 1;
+    if remDays < monLen then
+      break
+    remDays := remDays - monLen
+
+  let mday : Fin 31 := Fin.ofNat (Int.toNat remDays)
+
+  let hmon ←
+    if h₁ : mon.val > 10
+      then do
+        year := year + 1
+        pure (Month.Ordinal.ofNat (mon.val - 10) (by omega))
+      else
+        pure (Month.Ordinal.ofNat (mon.val + 2) (by omega))
+
+  let second : Bounded.LE 0 59 := remSecs.emod 60 (by decide)
+  let minute : Bounded.LE 0 59 := (remSecs.ediv 60 (by decide)).emod 60 (by decide)
+  let hour : Bounded.LE 0 23 := remSecs.ediv 3600 (by decide)
+  let nano : Bounded.LE 0 999999999 := Bounded.LE.byEmod nanos.val 1000000000 (by decide)
+
+  return {
+    date := PlainDate.ofYearMonthDayClip year hmon (Day.Ordinal.ofFin (Fin.succ mday))
+    time := PlainTime.ofHourMinuteSecondsNano (leap := false) (hour.expandTop (by decide)) minute second nano
+  }
+
+/--
+Converts a `PlainDateTime` to the number of days since the UNIX epoch.
+-/
+@[inline]
+def toDaysSinceUNIXEpoch (pdt : PlainDateTime) : Day.Offset :=
+  pdt.date.toDaysSinceUNIXEpoch
+
+/--
+Converts a `PlainDateTime` to the number of days since the UNIX epoch.
+-/
+@[inline]
+def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime) : PlainDateTime :=
+  PlainDateTime.mk (PlainDate.ofDaysSinceUNIXEpoch days) time
+
+/--
+Sets the `PlainDateTime` to the specified `desiredWeekday`.
+-/
+def withWeekday (dt : PlainDateTime) (desiredWeekday : Weekday) : PlainDateTime :=
+  { dt with date := PlainDate.withWeekday dt.date desiredWeekday }
+
+/--
+Creates a new `PlainDateTime` by adjusting the day of the month to the given `days` value, with any
+out-of-range days clipped to the nearest valid date.
+-/
+@[inline]
+def withDaysClip (dt : PlainDateTime) (days : Day.Ordinal) : PlainDateTime :=
+  { dt with date := PlainDate.ofYearMonthDayClip dt.date.year dt.date.month days }
+
+/--
+Creates a new `PlainDateTime` by adjusting the day of the month to the given `days` value, with any
+out-of-range days rolled over to the next month or year as needed.
+-/
+@[inline]
+def withDaysRollOver (dt : PlainDateTime) (days : Day.Ordinal) : PlainDateTime :=
+  { dt with date := PlainDate.rollOver dt.date.year dt.date.month days }
+
+/--
+Creates a new `PlainDateTime` by adjusting the month to the given `month` value, with any
+out-of-range days clipped to the nearest valid date.
+-/
+@[inline]
+def withMonthClip (dt : PlainDateTime) (month : Month.Ordinal) : PlainDateTime :=
+  { dt with date := PlainDate.ofYearMonthDayClip dt.date.year month dt.date.day }
+
+/--
+Creates a new `PlainDateTime` by adjusting the month to the given `month` value.
+The day is rolled over to the next valid month if necessary.
+-/
+@[inline]
+def withMonthRollOver (dt : PlainDateTime) (month : Month.Ordinal) : PlainDateTime :=
+  { dt with date := PlainDate.rollOver dt.date.year month dt.date.day }
+
+/--
+Creates a new `PlainDateTime` by adjusting the year to the given `year` value. The month and day
+remain unchanged, with any out-of-range days clipped to the nearest valid date.
+-/
+@[inline]
+def withYearClip (dt : PlainDateTime) (year : Year.Offset) : PlainDateTime :=
+  { dt with date := PlainDate.ofYearMonthDayClip year dt.date.month dt.date.day }
+
+/--
+Creates a new `PlainDateTime` by adjusting the year to the given `year` value. The month and day are rolled
+over to the next valid month and day if necessary.
+-/
+@[inline]
+def withYearRollOver (dt : PlainDateTime) (year : Year.Offset) : PlainDateTime :=
+  { dt with date := PlainDate.rollOver year dt.date.month dt.date.day }
+
+/--
+Creates a new `PlainDateTime` by adjusting the `hour` component of its `time` to the given value.
+-/
+@[inline]
+def withHours (dt : PlainDateTime) (hour : Hour.Ordinal) : PlainDateTime :=
+  { dt with time := { dt.time with hour := hour } }
+
+/--
+Creates a new `PlainDateTime` by adjusting the `minute` component of its `time` to the given value.
+-/
+@[inline]
+def withMinutes (dt : PlainDateTime) (minute : Minute.Ordinal) : PlainDateTime :=
+  { dt with time := { dt.time with minute := minute } }
+
+/--
+Creates a new `PlainDateTime` by adjusting the `second` component of its `time` to the given value.
+-/
+@[inline]
+def withSeconds (dt : PlainDateTime) (second : Sigma Second.Ordinal) : PlainDateTime :=
+  { dt with time := { dt.time with second := second } }
+
+/--
+Creates a new `PlainDateTime` by adjusting the milliseconds component inside the `nano` component of its `time` to the given value.
+-/
+@[inline]
+def withMilliseconds (dt : PlainDateTime) (millis : Millisecond.Ordinal) : PlainDateTime :=
+  { dt with time := dt.time.withMilliseconds millis }
+
+/--
+Creates a new `PlainDateTime` by adjusting the `nano` component of its `time` to the given value.
+-/
+@[inline]
+def withNanoseconds (dt : PlainDateTime) (nano : Nanosecond.Ordinal) : PlainDateTime :=
+  { dt with time := dt.time.withNanoseconds nano }
+
+/--
+Adds a `Day.Offset` to a `PlainDateTime`.
+-/
+@[inline]
+def addDays (dt : PlainDateTime) (days : Day.Offset) : PlainDateTime :=
+  { dt with date := dt.date.addDays days }
+
+/--
+Subtracts a `Day.Offset` from a `PlainDateTime`.
+-/
+@[inline]
+def subDays (dt : PlainDateTime) (days : Day.Offset) : PlainDateTime :=
+  { dt with date := dt.date.subDays days }
+
+/--
+Adds a `Week.Offset` to a `PlainDateTime`.
+-/
+@[inline]
+def addWeeks (dt : PlainDateTime) (weeks : Week.Offset) : PlainDateTime :=
+  { dt with date := dt.date.addWeeks weeks }
+
+/--
+Subtracts a `Week.Offset` from a `PlainDateTime`.
+-/
+@[inline]
+def subWeeks (dt : PlainDateTime) (weeks : Week.Offset) : PlainDateTime :=
+  { dt with date := dt.date.subWeeks weeks }
+
+/--
+Adds a `Month.Offset` to a `PlainDateTime`, adjusting the day to the last valid day of the resulting
+month.
+-/
+def addMonthsClip (dt : PlainDateTime) (months : Month.Offset) : PlainDateTime :=
+  { dt with date := dt.date.addMonthsClip months }
+
+/--
+Subtracts `Month.Offset` from a `PlainDateTime`, it clips the day to the last valid day of that month.
+-/
+@[inline]
+def subMonthsClip (dt : PlainDateTime) (months : Month.Offset) : PlainDateTime :=
+  { dt with date := dt.date.subMonthsClip months }
+
+/--
+Adds a `Month.Offset` to a `PlainDateTime`, rolling over excess days to the following month if needed.
+-/
+def addMonthsRollOver (dt : PlainDateTime) (months : Month.Offset) : PlainDateTime :=
+  { dt with date := dt.date.addMonthsRollOver months }
+
+/--
+Subtracts a `Month.Offset` from a `PlainDateTime`, adjusting the day to the last valid day of the
+resulting month.
+-/
+@[inline]
+def subMonthsRollOver (dt : PlainDateTime) (months : Month.Offset) : PlainDateTime :=
+  { dt with date := dt.date.subMonthsRollOver months }
+
+/--
+Adds a `Month.Offset` to a `PlainDateTime`, rolling over excess days to the following month if needed.
+-/
+@[inline]
+def addYearsRollOver (dt : PlainDateTime) (years : Year.Offset) : PlainDateTime :=
+  { dt with date := dt.date.addYearsRollOver years }
+
+/--
+Subtracts a `Month.Offset` from a `PlainDateTime`, rolling over excess days to the following month if
+needed.
+-/
+@[inline]
+def addYearsClip (dt : PlainDateTime) (years : Year.Offset) : PlainDateTime :=
+  { dt with date := dt.date.addYearsClip years }
+
+/--
+Subtracts a `Year.Offset` from a `PlainDateTime`, this function rolls over any excess days into the
+following month.
+-/
+@[inline]
+def subYearsRollOver (dt : PlainDateTime) (years : Year.Offset) : PlainDateTime :=
+  { dt with date := dt.date.subYearsRollOver years }
+
+/--
+Subtracts a `Year.Offset` from a `PlainDateTime`, adjusting the day to the last valid day of the
+resulting month.
+-/
+@[inline]
+def subYearsClip (dt : PlainDateTime) (years : Year.Offset) : PlainDateTime :=
+  { dt with date := dt.date.subYearsClip years }
+
+
+/--
+Adds an `Hour.Offset` to a `PlainDateTime`, adjusting the date if the hour overflows.
+-/
+@[inline]
+def addHours (dt : PlainDateTime) (hours : Hour.Offset) : PlainDateTime :=
+  let totalSeconds := dt.time.toSeconds + hours.toSeconds
+  let days := totalSeconds.ediv 86400
+  let newTime := dt.time.addSeconds (hours.toSeconds)
+  { dt with date := dt.date.addDays days, time := newTime }
+
+/--
+Subtracts an `Hour.Offset` from a `PlainDateTime`, adjusting the date if the hour underflows.
+-/
+@[inline]
+def subHours (dt : PlainDateTime) (hours : Hour.Offset) : PlainDateTime :=
+  addHours dt (-hours)
+
+/--
+Adds a `Minute.Offset` to a `PlainDateTime`, adjusting the hour and date if the minutes overflow.
+-/
+@[inline]
+def addMinutes (dt : PlainDateTime) (minutes : Minute.Offset) : PlainDateTime :=
+  let totalSeconds := dt.time.toSeconds + minutes.toSeconds
+  let days := totalSeconds.ediv 86400
+  let newTime := dt.time.addSeconds (minutes.toSeconds)
+  { dt with date := dt.date.addDays days, time := newTime }
+
+/--
+Subtracts a `Minute.Offset` from a `PlainDateTime`, adjusting the hour and date if the minutes underflow.
+-/
+@[inline]
+def subMinutes (dt : PlainDateTime) (minutes : Minute.Offset) : PlainDateTime :=
+  addMinutes dt (-minutes)
+
+/--
+Adds a `Second.Offset` to a `PlainDateTime`, adjusting the minute, hour, and date if the seconds overflow.
+-/
+@[inline]
+def addSeconds (dt : PlainDateTime) (seconds : Second.Offset) : PlainDateTime :=
+  let totalSeconds := dt.time.toSeconds + seconds
+  let days := totalSeconds.ediv 86400
+  let newTime := dt.time.addSeconds seconds
+  { dt with date := dt.date.addDays days, time := newTime }
+
+/--
+Subtracts a `Second.Offset` from a `PlainDateTime`, adjusting the minute, hour, and date if the seconds underflow.
+-/
+@[inline]
+def subSeconds (dt : PlainDateTime) (seconds : Second.Offset) : PlainDateTime :=
+  addSeconds dt (-seconds)
+
+/--
+Adds a `Millisecond.Offset` to a `PlainDateTime`, adjusting the second, minute, hour, and date if the milliseconds overflow.
+-/
+@[inline]
+def addMilliseconds (dt : PlainDateTime) (milliseconds : Millisecond.Offset) : PlainDateTime :=
+  let totalMilliseconds := dt.time.toMilliseconds + milliseconds
+  let days := totalMilliseconds.ediv 86400000 -- 86400000 ms in a day
+  let newTime := dt.time.addMilliseconds milliseconds
+  { dt with date := dt.date.addDays days, time := newTime }
+
+/--
+Subtracts a `Millisecond.Offset` from a `PlainDateTime`, adjusting the second, minute, hour, and date if the milliseconds underflow.
+-/
+@[inline]
+def subMilliseconds (dt : PlainDateTime) (milliseconds : Millisecond.Offset) : PlainDateTime :=
+  addMilliseconds dt (-milliseconds)
+
+/--
+Adds a `Nanosecond.Offset` to a `PlainDateTime`, adjusting the seconds, minutes, hours, and date if the nanoseconds overflow.
+-/
+@[inline]
+def addNanoseconds (dt : PlainDateTime) (nanos : Nanosecond.Offset) : PlainDateTime :=
+  let nano := Nanosecond.Offset.ofInt dt.time.nanosecond.val
+  let totalNanos := nano + nanos
+  let extraSeconds := totalNanos.ediv 1000000000
+  let nanosecond := Bounded.LE.byEmod totalNanos.val 1000000000 (by decide)
+  let newTime := dt.time.addSeconds extraSeconds
+  { dt with time := { newTime with nanosecond } }
+
+/--
+Subtracts a `Nanosecond.Offset` from a `PlainDateTime`, adjusting the seconds, minutes, hours, and date if the nanoseconds underflow.
+-/
+@[inline]
+def subNanoseconds (dt : PlainDateTime) (nanos : Nanosecond.Offset) : PlainDateTime :=
+  addNanoseconds dt (-nanos)
+
+/--
+Getter for the `Year` inside of a `PlainDateTime`.
+-/
+@[inline]
+def year (dt : PlainDateTime) : Year.Offset :=
+  dt.date.year
+
+/--
+Getter for the `Month` inside of a `PlainDateTime`.
+-/
+@[inline]
+def month (dt : PlainDateTime) : Month.Ordinal :=
+  dt.date.month
+
+/--
+Getter for the `Day` inside of a `PlainDateTime`.
+-/
+@[inline]
+def day (dt : PlainDateTime) : Day.Ordinal :=
+  dt.date.day
+
+/--
+Getter for the `Weekday` inside of a `PlainDateTime`.
+-/
+@[inline]
+def weekday (dt : PlainDateTime) : Weekday :=
+  dt.date.weekday
+
+/--
+Getter for the `Hour` inside of a `PlainDateTime`.
+-/
+@[inline]
+def hour (dt : PlainDateTime) : Hour.Ordinal :=
+  dt.time.hour
+
+/--
+Getter for the `Minute` inside of a `PlainDateTime`.
+-/
+@[inline]
+def minute (dt : PlainDateTime) : Minute.Ordinal :=
+  dt.time.minute
+
+/--
+Getter for the `Millisecond` inside of a `PlainDateTime`.
+-/
+@[inline]
+def millisecond (dt : PlainDateTime) : Millisecond.Ordinal :=
+  dt.time.millisecond
+
+/--
+Getter for the `Second` inside of a `PlainDateTime`.
+-/
+@[inline]
+def second (dt : PlainDateTime) : Second.Ordinal dt.time.second.fst :=
+  dt.time.second.snd
+
+/--
+Getter for the `Nanosecond.Ordinal` inside of a `PlainDateTime`.
+-/
+@[inline]
+def nanosecond (dt : PlainDateTime) : Nanosecond.Ordinal :=
+  dt.time.nanosecond
+
+/--
+Determines the era of the given `PlainDateTime` based on its year.
+-/
+@[inline]
+def era (date : PlainDateTime) : Year.Era :=
+  date.date.era
+
+/--
+Checks if the `PlainDateTime` is in a leap year.
+-/
+@[inline]
+def inLeapYear (date : PlainDateTime) : Bool :=
+  date.year.isLeap
+
+/--
+Determines the week of the year for the given `PlainDateTime`.
+-/
+@[inline]
+def weekOfYear (date : PlainDateTime) : Week.Ordinal :=
+  date.date.weekOfYear
+
+/--
+Returns the unaligned week of the month for a `PlainDateTime` (day divided by 7, plus 1).
+-/
+def weekOfMonth (date : PlainDateTime) : Bounded.LE 1 5 :=
+  date.date.weekOfMonth
+
+/--
+Determines the week of the month for the given `PlainDateTime`. The week of the month is calculated based
+on the day of the month and the weekday. Each week starts on Monday because the entire library is
+based on the Gregorian Calendar.
+-/
+@[inline]
+def alignedWeekOfMonth (date : PlainDateTime) : Week.Ordinal.OfMonth :=
+  date.date.alignedWeekOfMonth
+
+/--
+Transforms a tuple of a `PlainDateTime` into a `Day.Ordinal.OfYear`.
+-/
+@[inline]
+def dayOfYear (date : PlainDateTime) : Day.Ordinal.OfYear date.year.isLeap :=
+  ValidDate.dayOfYear ⟨(date.month, date.day), date.date.valid⟩
+
+/--
+Determines the quarter of the year for the given `PlainDateTime`.
+-/
+@[inline]
+def quarter (date : PlainDateTime) : Bounded.LE 1 4 :=
+  date.date.quarter
+
+/--
+Combines a `PlainDate` and `PlainTime` into a `PlainDateTime`.
+-/
+@[inline]
+def atTime : PlainDate → PlainTime → PlainDateTime :=
+  PlainDateTime.mk
+
+/--
+Combines a `PlainTime` and `PlainDate` into a `PlainDateTime`.
+-/
+@[inline]
+def atDate (time: PlainTime) (date: PlainDate) : PlainDateTime :=
+  PlainDateTime.mk date time
+
+instance : HAdd PlainDateTime Day.Offset PlainDateTime where
+  hAdd := addDays
+
+instance : HSub PlainDateTime Day.Offset PlainDateTime where
+  hSub := subDays
+
+instance : HAdd PlainDateTime Week.Offset PlainDateTime where
+  hAdd := addWeeks
+
+instance : HSub PlainDateTime Week.Offset PlainDateTime where
+  hSub := subWeeks
+
+instance : HAdd PlainDateTime Hour.Offset PlainDateTime where
+  hAdd := addHours
+
+instance : HSub PlainDateTime Hour.Offset PlainDateTime where
+  hSub := subHours
+
+instance : HAdd PlainDateTime Minute.Offset PlainDateTime where
+  hAdd := addMinutes
+
+instance : HSub PlainDateTime Minute.Offset PlainDateTime where
+  hSub := subMinutes
+
+instance : HAdd PlainDateTime Millisecond.Offset PlainDateTime where
+  hAdd := addMilliseconds
+
+instance : HSub PlainDateTime Millisecond.Offset PlainDateTime where
+  hSub := addMilliseconds
+
+instance : HAdd PlainDateTime Second.Offset PlainDateTime where
+  hAdd := addSeconds
+
+instance : HSub PlainDateTime Second.Offset PlainDateTime where
+  hSub := subSeconds
+
+instance : HAdd PlainDateTime Nanosecond.Offset PlainDateTime where
+  hAdd := addNanoseconds
+
+instance : HSub PlainDateTime Nanosecond.Offset PlainDateTime where
+  hSub := subNanoseconds
+
+instance : HAdd PlainDateTime Duration PlainDateTime where
+  hAdd x y := addNanoseconds x y.toNanoseconds
+
+end PlainDateTime
+namespace PlainDate
+
+/--
+Combines a `PlainDate` and `PlainTime` into a `PlainDateTime`.
+-/
+@[inline]
+def atTime : PlainDate → PlainTime → PlainDateTime :=
+  PlainDateTime.mk
+
+end PlainDate
+namespace PlainTime
+
+/--
+Combines a `PlainTime` and `PlainDate` into a `PlainDateTime`.
+-/
+@[inline]
+def atDate (time: PlainTime) (date: PlainDate) : PlainDateTime :=
+  PlainDateTime.mk date time
+
+end PlainTime
+end Time
+end Std

src/Std/Time/DateTime/Timestamp.lean

@@ -0,0 +1,289 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+prelude
+import Std.Time.Internal
+import Init.Data.Int
+import Std.Time.Time
+import Std.Time.Date
+import Std.Time.Duration
+
+namespace Std
+namespace Time
+open Internal
+
+set_option linter.all true
+
+/--
+Represents an exact point in time as a UNIX Epoch timestamp.
+-/
+structure Timestamp where
+
+  /--
+  Duration since the unix epoch.
+  -/
+  val : Duration
+  deriving Repr, BEq, Inhabited
+
+instance : LE Timestamp where
+  le x y := x.val ≤ y.val
+
+instance { x y : Timestamp } : Decidable (x ≤ y) :=
+  inferInstanceAs (Decidable (x.val ≤ y.val))
+
+instance : OfNat Timestamp n where
+  ofNat := ⟨OfNat.ofNat n⟩
+
+instance : ToString Timestamp where
+  toString s := toString s.val.toMilliseconds
+
+instance : Repr Timestamp where
+  reprPrec s := reprPrec (toString s)
+
+namespace Timestamp
+
+/--
+Fetches the current duration from the system.
+-/
+@[extern "lean_get_current_time"]
+opaque now : IO Timestamp
+
+/--
+Converts a `Timestamp` to minutes as `Minute.Offset`.
+-/
+@[inline]
+def toMinutes (tm : Timestamp) : Minute.Offset :=
+  tm.val.second.ediv 60
+
+/--
+Converts a `Timestamp` to days as `Day.Offset`.
+-/
+@[inline]
+def toDays (tm : Timestamp) : Day.Offset :=
+  tm.val.second.ediv 86400
+
+/--
+Creates a `Timestamp` from a `Second.Offset` since the Unix epoch.
+-/
+@[inline]
+def ofSecondsSinceUnixEpoch (secs : Second.Offset) : Timestamp :=
+  ⟨Duration.ofSeconds secs⟩
+
+/--
+Creates a `Timestamp` from a `Nanosecond.Offset` since the Unix epoch.
+-/
+@[inline]
+def ofNanosecondsSinceUnixEpoch (nanos : Nanosecond.Offset) : Timestamp :=
+  ⟨Duration.ofNanoseconds nanos⟩
+
+/--
+Creates a `Timestamp` from a `Millisecond.Offset` since the Unix epoch.
+-/
+@[inline]
+def ofMillisecondsSinceUnixEpoch (milli : Millisecond.Offset) : Timestamp :=
+  ⟨Duration.ofNanoseconds milli.toNanoseconds⟩
+
+/--
+Converts a `Timestamp` to seconds as `Second.Offset`.
+-/
+@[inline]
+def toSecondsSinceUnixEpoch (t : Timestamp) : Second.Offset :=
+  t.val.second
+
+/--
+Converts a `Timestamp` to nanoseconds as `Nanosecond.Offset`.
+-/
+@[inline]
+def toNanosecondsSinceUnixEpoch (tm : Timestamp) : Nanosecond.Offset :=
+  let nanos := tm.toSecondsSinceUnixEpoch.mul 1000000000
+  let nanos := nanos + (.ofInt tm.val.nano.val)
+  nanos
+
+/--
+Converts a `Timestamp` to nanoseconds as `Millisecond.Offset`.
+-/
+@[inline]
+def toMillisecondsSinceUnixEpoch (tm : Timestamp) : Millisecond.Offset :=
+  tm.toNanosecondsSinceUnixEpoch.toMilliseconds
+
+/--
+Calculates the duration from the given `Timestamp` to the current time.
+-/
+@[inline]
+def since (f : Timestamp) : IO Duration := do
+  let cur ← Timestamp.now
+  return Std.Time.Duration.sub cur.val f.val
+
+/--
+Returns the `Duration` represented by the `Timestamp` since the Unix epoch.
+-/
+@[inline]
+def toDurationSinceUnixEpoch (tm : Timestamp) : Duration :=
+  tm.val
+
+/--
+Adds a `Millisecond.Offset` to the given `Timestamp`.
+-/
+@[inline]
+def addMilliseconds (t : Timestamp) (s : Millisecond.Offset) : Timestamp :=
+  ⟨t.val + s⟩
+
+/--
+Subtracts a `Millisecond.Offset` from the given `Timestamp`.
+-/
+@[inline]
+def subMilliseconds (t : Timestamp) (s : Millisecond.Offset) : Timestamp :=
+  ⟨t.val - s⟩
+
+/--
+Adds a `Nanosecond.Offset` to the given `Timestamp`.
+-/
+@[inline]
+def addNanoseconds (t : Timestamp) (s : Nanosecond.Offset) : Timestamp :=
+  ⟨t.val + s⟩
+
+/--
+Subtracts a `Nanosecond.Offset` from the given `Timestamp`.
+-/
+@[inline]
+def subNanoseconds (t : Timestamp) (s : Nanosecond.Offset) : Timestamp :=
+  ⟨t.val - s⟩
+
+/--
+Adds a `Second.Offset` to the given `Timestamp`.
+-/
+@[inline]
+def addSeconds (t : Timestamp) (s : Second.Offset) : Timestamp :=
+  ⟨t.val + s⟩
+
+/--
+Subtracts a `Second.Offset` from the given `Timestamp`.
+-/
+@[inline]
+def subSeconds (t : Timestamp) (s : Second.Offset) : Timestamp :=
+  ⟨t.val - s⟩
+
+/--
+Adds a `Minute.Offset` to the given `Timestamp`.
+-/
+@[inline]
+def addMinutes (t : Timestamp) (m : Minute.Offset) : Timestamp :=
+  ⟨t.val + m⟩
+
+/--
+Subtracts a `Minute.Offset` from the given `Timestamp`.
+-/
+@[inline]
+def subMinutes (t : Timestamp) (m : Minute.Offset) : Timestamp :=
+  ⟨t.val - m⟩
+
+/--
+Adds an `Hour.Offset` to the given `Timestamp`.
+-/
+@[inline]
+def addHours (t : Timestamp) (h : Hour.Offset) : Timestamp :=
+  ⟨t.val + h⟩
+
+/--
+Subtracts an `Hour.Offset` from the given `Timestamp`.
+-/
+@[inline]
+def subHours (t : Timestamp) (h : Hour.Offset) : Timestamp :=
+  ⟨t.val - h⟩
+
+/--
+Adds a `Day.Offset` to the given `Timestamp`.
+-/
+@[inline]
+def addDays (t : Timestamp) (d : Day.Offset) : Timestamp :=
+  ⟨t.val + d⟩
+
+/--
+Subtracts a `Day.Offset` from the given `Timestamp`.
+-/
+@[inline]
+def subDays (t : Timestamp) (d : Day.Offset) : Timestamp :=
+  ⟨t.val - d⟩
+
+/--
+Adds a `Week.Offset` to the given `Timestamp`.
+-/
+@[inline]
+def addWeeks (t : Timestamp) (d : Week.Offset) : Timestamp :=
+  ⟨t.val + d⟩
+
+/--
+Subtracts a `Week.Offset` from the given `Timestamp`.
+-/
+@[inline]
+def subWeeks (t : Timestamp) (d : Week.Offset) : Timestamp :=
+  ⟨t.val - d⟩
+
+/--
+Adds a `Duration` to the given `Timestamp`.
+-/
+@[inline]
+def addDuration (t : Timestamp) (d : Duration) : Timestamp :=
+  ⟨t.val + d⟩
+
+/--
+Subtracts a `Duration` from the given `Timestamp`.
+-/
+@[inline]
+def subDuration (t : Timestamp) (d : Duration) : Timestamp :=
+  ⟨t.val - d⟩
+
+instance : HAdd Timestamp Duration Timestamp where
+  hAdd := addDuration
+
+instance : HSub Timestamp Duration Timestamp where
+  hSub := subDuration
+
+instance : HAdd Timestamp Day.Offset Timestamp where
+  hAdd := addDays
+
+instance : HSub Timestamp Day.Offset Timestamp where
+  hSub := subDays
+
+instance : HAdd Timestamp Week.Offset Timestamp where
+  hAdd := addWeeks
+
+instance : HSub Timestamp Week.Offset Timestamp where
+  hSub := subWeeks
+
+instance : HAdd Timestamp Hour.Offset Timestamp where
+  hAdd := addHours
+
+instance : HSub Timestamp Hour.Offset Timestamp where
+  hSub := subHours
+
+instance : HAdd Timestamp Minute.Offset Timestamp where
+  hAdd := addMinutes
+
+instance : HSub Timestamp Minute.Offset Timestamp where
+  hSub := subMinutes
+
+instance : HAdd Timestamp Second.Offset Timestamp where
+  hAdd := addSeconds
+
+instance : HSub Timestamp Second.Offset Timestamp where
+  hSub := subSeconds
+
+instance : HAdd Timestamp Millisecond.Offset Timestamp where
+  hAdd := addMilliseconds
+
+instance : HSub Timestamp Millisecond.Offset Timestamp where
+  hSub := subMilliseconds
+
+instance : HAdd Timestamp Nanosecond.Offset Timestamp where
+  hAdd := addNanoseconds
+
+instance : HSub Timestamp Nanosecond.Offset Timestamp where
+  hSub := subNanoseconds
+
+instance : HSub Timestamp Timestamp Duration where
+  hSub x y := x.val - y.val
+
+end Timestamp