fix: verso test

Undo namespace collapses (e.g. `namespace Std.Time.Day.Offset`) back to
the original multi-line form (`namespace Std / namespace Time / namespace Day`),
keeping only functional formatting and parsing changes in this PR.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

src/Lean/Meta/Sym.lean

@@ -25,7 +25,6 @@ public import Lean.Meta.Sym.Simp
 public import Lean.Meta.Sym.Util
 public import Lean.Meta.Sym.Eta
 public import Lean.Meta.Sym.Canon
-public import Lean.Meta.Sym.Arith
 public import Lean.Meta.Sym.Grind
 public import Lean.Meta.Sym.SynthInstance
 

src/Lean/Meta/Sym/Arith.lean

@@ -1,20 +0,0 @@
-/-
-Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Sym.Arith.Types
-public import Lean.Meta.Sym.Arith.EvalNum
-public import Lean.Meta.Sym.Arith.Classify
-public import Lean.Meta.Sym.Arith.MonadCanon
-public import Lean.Meta.Sym.Arith.MonadRing
-public import Lean.Meta.Sym.Arith.MonadSemiring
-public import Lean.Meta.Sym.Arith.MonadVar
-public import Lean.Meta.Sym.Arith.Functions
-public import Lean.Meta.Sym.Arith.Reify
-public import Lean.Meta.Sym.Arith.DenoteExpr
-public import Lean.Meta.Sym.Arith.ToExpr
-public import Lean.Meta.Sym.Arith.VarRename
-public import Lean.Meta.Sym.Arith.Poly

src/Lean/Meta/Sym/Arith/Classify.lean

@@ -1,143 +0,0 @@
-/-
-Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Sym.Arith.EvalNum
-import Lean.Meta.Sym.SynthInstance
-import Lean.Meta.Sym.Canon
-import Lean.Meta.DecLevel
-import Init.Grind.Ring
-public section
-
-namespace Lean.Meta.Sym.Arith
-
-/-!
-# Algebraic structure classification
-
-Detects the strongest algebraic structure available for a type and caches
-the classification in `Arith.State.typeClassify`. The detection order is:
-
-1. `Grind.CommRing` (includes `Field` check)
-2. `Grind.Ring` (non-commutative)
-3. `Grind.CommSemiring` (via `OfSemiring.Q` envelope)
-4. `Grind.Semiring` (non-commutative)
-
-Results (including failures) are cached in a single `PHashMap ExprPtr ClassifyResult`
-to avoid repeated synthesis attempts.
--/
-
-private def getIsCharInst? (u : Level) (type : Expr) (semiringInst : Expr) : SymM (Option (Expr × Nat)) := do
-  withNewMCtxDepth do
-    let n ← mkFreshExprMVar (mkConst ``Nat)
-    let charType := mkApp3 (mkConst ``Grind.IsCharP [u]) type semiringInst n
-    let some charInst ← Sym.synthInstance? charType | return none
-    let n ← instantiateMVars n
-    let some n ← evalNat? n | return none
-    return some (charInst, n)
-
-private def getNoZeroDivInst? (u : Level) (type : Expr) : SymM (Option Expr) := do
-  let natModuleType := mkApp (mkConst ``Grind.NatModule [u]) type
-  let some natModuleInst ← Sym.synthInstance? natModuleType | return none
-  let noZeroDivType := mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type natModuleInst
-  Sym.synthInstance? noZeroDivType
-
-/-- Try to classify `type` as a `CommRing`. Returns the ring id on success. -/
-private def tryCommRing? (type : Expr) : SymM (Option Nat) := do
-  let u ← getDecLevel type
-  let commRing := mkApp (mkConst ``Grind.CommRing [u]) type
-  let some commRingInst ← Sym.synthInstance? commRing | return none
-  let ringInst := mkApp2 (mkConst ``Grind.CommRing.toRing [u]) type commRingInst
-  let semiringInst := mkApp2 (mkConst ``Grind.Ring.toSemiring [u]) type ringInst
-  let commSemiringInst := mkApp2 (mkConst ``Grind.CommRing.toCommSemiring [u]) type semiringInst
-  let charInst? ← getIsCharInst? u type semiringInst
-  let noZeroDivInst? ← getNoZeroDivInst? u type
-  let fieldInst? ← Sym.synthInstance? <| mkApp (mkConst ``Grind.Field [u]) type
-  let semiringId? := none
-  let id := (← getArithState).rings.size
-  let ring : CommRing := {
-    id, semiringId?, type, u, semiringInst, ringInst, commSemiringInst,
-    commRingInst, charInst?, noZeroDivInst?, fieldInst?,
-  }
-  modifyArithState fun s => { s with rings := s.rings.push ring }
-  return some id
-
-/-- Try to classify `type` as a non-commutative `Ring`. -/
-private def tryNonCommRing? (type : Expr) : SymM (Option Nat) := do
-  let u ← getDecLevel type
-  let ring := mkApp (mkConst ``Grind.Ring [u]) type
-  let some ringInst ← Sym.synthInstance? ring | return none
-  let semiringInst := mkApp2 (mkConst ``Grind.Ring.toSemiring [u]) type ringInst
-  let charInst? ← getIsCharInst? u type semiringInst
-  let id := (← getArithState).ncRings.size
-  let ring : Ring := {
-    id, type, u, semiringInst, ringInst, charInst?
-  }
-  modifyArithState fun s => { s with ncRings := s.ncRings.push ring }
-  return some id
-
-/-- Helper function for `tryCommSemiring? -/
-private def tryCacheAndCommRing? (type : Expr) : SymM (Option Nat) := do
-  if let some result := (← getArithState).typeClassify.find? { expr := type } then
-    let .commRing id := result | return none
-    return id
-  let id? ← tryCommRing? type
-  let result := match id? with
-    | none => .none
-    | some id => .commRing id
-  modifyArithState fun s => { s with typeClassify := s.typeClassify.insert { expr := type } result }
-  return id?
-
-/-- Try to classify `type` as a `CommSemiring`. Creates the `OfSemiring.Q` envelope ring. -/
-private def tryCommSemiring? (type : Expr) : SymM (Option Nat) := do
-  let u ← getDecLevel type
-  let commSemiring := mkApp (mkConst ``Grind.CommSemiring [u]) type
-  let some commSemiringInst ← Sym.synthInstance? commSemiring | return none
-  let semiringInst := mkApp2 (mkConst ``Grind.CommSemiring.toSemiring [u]) type commSemiringInst
-  let q ← shareCommon (← Sym.canon (mkApp2 (mkConst ``Grind.Ring.OfSemiring.Q [u]) type semiringInst))
-  -- The envelope `Q` type must be classifiable as a CommRing.
-  let some ringId ← tryCacheAndCommRing? q
-    | reportIssue! "unexpected failure initializing ring{indentExpr q}"; return none
-  let id := (← getArithState).semirings.size
-  let semiring : CommSemiring := {
-    id, type, ringId, u, semiringInst, commSemiringInst
-  }
-  modifyArithState fun s => { s with semirings := s.semirings.push semiring }
-  -- Link the envelope ring back to this semiring
-  modifyArithState fun s =>
-    let rings := s.rings.modify ringId fun r => { r with semiringId? := some id }
-    { s with rings }
-  return some id
-
-/-- Try to classify `type` as a non-commutative `Semiring`. -/
-private def tryNonCommSemiring? (type : Expr) : SymM (Option Nat) := do
-  let u ← getDecLevel type
-  let semiring := mkApp (mkConst ``Grind.Semiring [u]) type
-  let some semiringInst ← Sym.synthInstance? semiring | return none
-  let id := (← getArithState).ncSemirings.size
-  let semiring : Semiring := { id, type, u, semiringInst }
-  modifyArithState fun s => { s with ncSemirings := s.ncSemirings.push semiring }
-  return some id
-
-/--
-Classify the algebraic structure of `type`, trying the strongest first:
-CommRing > Ring > CommSemiring > Semiring.
-Results are cached in `Arith.State.typeClassify`.
--/
-def classify? (type : Expr) : SymM ClassifyResult := do
-  if let some result := (← getArithState).typeClassify.find? { expr := type } then
-    return result
-  let result ← go
-  modifyArithState fun s => { s with typeClassify := s.typeClassify.insert { expr := type } result }
-  return result
-where
-  go : SymM ClassifyResult := do
-    if let some id ← tryCommRing? type then return .commRing id
-    if let some id ← tryNonCommRing? type then return .nonCommRing id
-    if let some id ← tryCommSemiring? type then return .commSemiring id
-    if let some id ← tryNonCommSemiring? type then return .nonCommSemiring id
-    return .none
-
-end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/DenoteExpr.lean

@@ -1,93 +0,0 @@
-/-
-Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Sym.Arith.Functions
-public import Lean.Meta.Sym.Arith.MonadVar
-public section
-namespace Lean.Meta.Sym.Arith
-
-/-!
-# Denotation of reified expressions
-
-Converts reified `RingExpr`, `Poly`, `Mon`, `Power` back into Lean `Expr`s using
-the ring's cached operator functions and variable array.
--/
-
-variable [Monad m] [MonadError m] [MonadLiftT MetaM m] [MonadCanon m] [MonadRing m]
-
-/-- Convert an integer to a numeral expression in the ring. Negative values use `getNegFn`. -/
-def denoteNum (k : Int) : m Expr := do
-  let ring ← getRing
-  let n := mkRawNatLit k.natAbs
-  let ofNatInst ← if let some inst ← MonadCanon.synthInstance? (mkApp2 (mkConst ``OfNat [ring.u]) ring.type n) then
-    pure inst
-  else
-    pure <| mkApp3 (mkConst ``Grind.Semiring.ofNat [ring.u]) ring.type ring.semiringInst n
-  let e := mkApp3 (mkConst ``OfNat.ofNat [ring.u]) ring.type n ofNatInst
-  if k < 0 then
-    return mkApp (← getNegFn) e
-  else
-    return e
-
-/-- Denote a `Power` (variable raised to a power). -/
-def denotePower [MonadGetVar m] (pw : Power) : m Expr := do
-  let x ← getVar pw.x
-  if pw.k == 1 then
-    return x
-  else
-    return mkApp2 (← getPowFn) x (toExpr pw.k)
-
-/-- Denote a `Mon` (product of powers). -/
-def denoteMon [MonadGetVar m] (mn : Mon) : m Expr := do
-  match mn with
-  | .unit => denoteNum 1
-  | .mult pw mn => go mn (← denotePower pw)
-where
-  go (mn : Mon) (acc : Expr) : m Expr := do
-    match mn with
-    | .unit => return acc
-    | .mult pw mn => go mn (mkApp2 (← getMulFn) acc (← denotePower pw))
-
-/-- Denote a `Poly` (sum of coefficient × monomial terms). -/
-def denotePoly [MonadGetVar m] (p : Poly) : m Expr := do
-  match p with
-  | .num k => denoteNum k
-  | .add k mn p => go p (← denoteTerm k mn)
-where
-  denoteTerm (k : Int) (mn : Mon) : m Expr := do
-    if k == 1 then
-      denoteMon mn
-    else
-      return mkApp2 (← getMulFn) (← denoteNum k) (← denoteMon mn)
-
-  go (p : Poly) (acc : Expr) : m Expr := do
-    match p with
-    | .num 0 => return acc
-    | .num k => return mkApp2 (← getAddFn) acc (← denoteNum k)
-    | .add k mn p => go p (mkApp2 (← getAddFn) acc (← denoteTerm k mn))
-
-/-- Denote a `RingExpr` using a variable lookup function. -/
-@[specialize]
-private def denoteRingExprCore (getVarExpr : Nat → Expr) (e : RingExpr) : m Expr := do
-  go e
-where
-  go : RingExpr → m Expr
-  | .num k => denoteNum k
-  | .natCast k => return mkApp (← getNatCastFn) (mkNatLit k)
-  | .intCast k => return mkApp (← getIntCastFn) (mkIntLit k)
-  | .var x => return getVarExpr x
-  | .add a b => return mkApp2 (← getAddFn) (← go a) (← go b)
-  | .sub a b => return mkApp2 (← getSubFn) (← go a) (← go b)
-  | .mul a b => return mkApp2 (← getMulFn) (← go a) (← go b)
-  | .pow a k => return mkApp2 (← getPowFn) (← go a) (toExpr k)
-  | .neg a => return mkApp (← getNegFn) (← go a)
-
-/-- Denote a `RingExpr` using an explicit variable array. -/
-def denoteRingExpr (vars : Array Expr) (e : RingExpr) : m Expr := do
-  denoteRingExprCore (fun x => vars[x]!) e
-
-end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/EvalNum.lean

@@ -1,90 +0,0 @@
-/-
-Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Sym.Arith.Types
-import Lean.Meta.Sym.LitValues
-import Lean.Meta.IntInstTesters
-import Lean.Meta.NatInstTesters
-public section
-
-namespace Lean.Meta.Sym.Arith
-
-/-!
-Functions for evaluating simple `Nat` and `Int` expressions that appear in type classes
-(e.g., `ToInt` and `IsCharP`). Using `whnf` for this purpose is too expensive and can
-exhaust the stack. We considered `evalExpr` as an alternative, but it introduces
-considerable overhead. We may use `evalExpr` as a fallback in the future.
--/
-
-def checkExp (k : Nat) : OptionT SymM Unit := do
-  let exp ← getExpThreshold
-  if k > exp then
-    reportIssue! "exponent {k} exceeds threshold for exponentiation `(exp := {exp})`"
-    failure
-
-/-
-**Note**: It is safe to use (the more efficient) structural instance tests here because
-`Sym.Canon` has already run.
--/
-open Structural in
-mutual
-private partial def evalNatCore (e : Expr) : OptionT SymM Nat := do
-  match_expr e with
-  | Nat.zero => return 0
-  | Nat.succ a => return (← evalNatCore a) + 1
-  | Int.toNat a => return (← evalIntCore a).toNat
-  | Int.natAbs a => return (← evalIntCore a).natAbs
-  | HAdd.hAdd _ _ _ inst a b => guard (← isInstHAddNat inst); return (← evalNatCore a) + (← evalNatCore b)
-  | HMul.hMul _ _ _ inst a b => guard (← isInstHMulNat inst); return (← evalNatCore a) * (← evalNatCore b)
-  | HSub.hSub _ _ _ inst a b => guard (← isInstHSubNat inst); return (← evalNatCore a) - (← evalNatCore b)
-  | HDiv.hDiv _ _ _ inst a b => guard (← isInstHDivNat inst); return (← evalNatCore a) / (← evalNatCore b)
-  | HMod.hMod _ _ _ inst a b => guard (← isInstHModNat inst); return (← evalNatCore a) % (← evalNatCore b)
-  | OfNat.ofNat _ _ _ =>
-    let some n := Sym.getNatValue? e |>.run | failure
-    return n
-  | HPow.hPow _ _ _ inst a k =>
-    guard (← isInstHPowNat inst)
-    let k ← evalNatCore k
-    checkExp k
-    let a ← evalNatCore a
-    return a ^ k
-  | _ => failure
-
-private partial def evalIntCore (e : Expr) : OptionT SymM Int := do
-  match_expr e with
-  | Neg.neg _ i a => guard (← isInstNegInt i); return - (← evalIntCore a)
-  | HAdd.hAdd _ _ _ i a b => guard (← isInstHAddInt i); return (← evalIntCore a) + (← evalIntCore b)
-  | HSub.hSub _ _ _ i a b => guard (← isInstHSubInt i); return (← evalIntCore a) - (← evalIntCore b)
-  | HMul.hMul _ _ _ i a b => guard (← isInstHMulInt i); return (← evalIntCore a) * (← evalIntCore b)
-  | HDiv.hDiv _ _ _ i a b => guard (← isInstHDivInt i); return (← evalIntCore a) / (← evalIntCore b)
-  | HMod.hMod _ _ _ i a b => guard (← isInstHModInt i); return (← evalIntCore a) % (← evalIntCore b)
-  | HPow.hPow _ _ _ i a k =>
-    guard (← isInstHPowInt i)
-    let a ← evalIntCore a
-    let k ← evalNatCore k
-    checkExp k
-    return a ^ k
-  | OfNat.ofNat _ _ _ =>
-    let some n := Sym.getIntValue? e |>.run | failure
-    return n
-  | NatCast.natCast _ i a =>
-    let_expr instNatCastInt ← i | failure
-    return (← evalNatCore a)
-  | Nat.cast _ i a =>
-    let_expr instNatCastInt ← i | failure
-    return (← evalNatCore a)
-  | _ => failure
-
-end
-
-def evalNat? (e : Expr) : SymM (Option Nat) :=
-  evalNatCore e |>.run
-
-def evalInt? (e : Expr) : SymM (Option Int) :=
-  evalIntCore e |>.run
-
-end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/Functions.lean

@@ -1,171 +0,0 @@
-/-
-Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Sym.Arith.MonadRing
-public import Lean.Meta.Sym.Arith.MonadSemiring
-public section
-namespace Lean.Meta.Sym.Arith
-
-/-!
-# Cached function expressions for arithmetic operators
-
-Synthesizes and caches the canonical Lean expressions for arithmetic operators
-(`+`, `*`, `-`, `^`, `intCast`, `natCast`, etc.). These cached expressions are used
-during reification to validate instances via pointer equality (`isSameExpr`).
-
-Each getter checks the cache field first. On a miss, it synthesizes the instance,
-verifies it against the expected instance from the ring structure using `isDefEqI`,
-canonicalizes the result via `canonExpr`, and stores it.
--/
-
-variable [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m]
-
-private def checkInst (declName : Name) (inst inst' : Expr) : MetaM Unit := do
-  unless (← withReducibleAndInstances <| isDefEq inst inst') do
-    throwError "error while initializing arithmetic operators:\ninstance for `{declName}` {indentExpr inst}\nis not definitionally equal to the expected one {indentExpr inst'}\nwhen only reducible definitions and instances are reduced"
-
-private def mkUnaryFn (type : Expr) (u : Level) (instDeclName : Name) (declName : Name) (expectedInst : Expr) : m Expr := do
-  let inst ← MonadCanon.synthInstance <| mkApp (mkConst instDeclName [u]) type
-  checkInst declName inst expectedInst
-  canonExpr <| mkApp2 (mkConst declName [u]) type inst
-
-private def mkBinHomoFn (type : Expr) (u : Level) (instDeclName : Name) (declName : Name) (expectedInst : Expr) : m Expr := do
-  let inst ← MonadCanon.synthInstance <| mkApp3 (mkConst instDeclName [u, u, u]) type type type
-  checkInst declName inst expectedInst
-  canonExpr <| mkApp4 (mkConst declName [u, u, u]) type type type inst
-
-private def mkPowFn (u : Level) (type : Expr) (semiringInst : Expr) : m Expr := do
-  let inst ← MonadCanon.synthInstance <| mkApp3 (mkConst ``HPow [u, 0, u]) type Nat.mkType type
-  let inst' := mkApp2 (mkConst ``Grind.Semiring.npow [u]) type semiringInst
-  checkInst ``HPow.hPow inst inst'
-  canonExpr <| mkApp4 (mkConst ``HPow.hPow [u, 0, u]) type Nat.mkType type inst
-
-private def mkNatCastFn (u : Level) (type : Expr) (semiringInst : Expr) : m Expr := do
-  let inst' := mkApp2 (mkConst ``Grind.Semiring.natCast [u]) type semiringInst
-  let instType := mkApp (mkConst ``NatCast [u]) type
-  -- Note: `Semiring.natCast` is not a global instance, so `NatCast α` may not be available.
-  -- When present, verify defeq; otherwise fall back to the semiring field.
-  let inst ← match (← MonadCanon.synthInstance? instType) with
-  | none => pure inst'
-  | some inst => checkInst ``NatCast.natCast inst inst'; pure inst
-  canonExpr <| mkApp2 (mkConst ``NatCast.natCast [u]) type inst
-
-section RingFns
-variable [MonadRing m]
-
-def getAddFn : m Expr := do
-  let ring ← getRing
-  if let some addFn := ring.addFn? then return addFn
-  let expectedInst := mkApp2 (mkConst ``instHAdd [ring.u]) ring.type <| mkApp2 (mkConst ``Grind.Semiring.toAdd [ring.u]) ring.type ring.semiringInst
-  let addFn ← mkBinHomoFn ring.type ring.u ``HAdd ``HAdd.hAdd expectedInst
-  modifyRing fun s => { s with addFn? := some addFn }
-  return addFn
-
-def getMulFn : m Expr := do
-  let ring ← getRing
-  if let some mulFn := ring.mulFn? then return mulFn
-  let expectedInst := mkApp2 (mkConst ``instHMul [ring.u]) ring.type <| mkApp2 (mkConst ``Grind.Semiring.toMul [ring.u]) ring.type ring.semiringInst
-  let mulFn ← mkBinHomoFn ring.type ring.u ``HMul ``HMul.hMul expectedInst
-  modifyRing fun s => { s with mulFn? := some mulFn }
-  return mulFn
-
-def getSubFn : m Expr := do
-  let ring ← getRing
-  if let some subFn := ring.subFn? then return subFn
-  let expectedInst := mkApp2 (mkConst ``instHSub [ring.u]) ring.type <| mkApp2 (mkConst ``Grind.Ring.toSub [ring.u]) ring.type ring.ringInst
-  let subFn ← mkBinHomoFn ring.type ring.u ``HSub ``HSub.hSub expectedInst
-  modifyRing fun s => { s with subFn? := some subFn }
-  return subFn
-
-def getNegFn : m Expr := do
-  let ring ← getRing
-  if let some negFn := ring.negFn? then return negFn
-  let expectedInst := mkApp2 (mkConst ``Grind.Ring.toNeg [ring.u]) ring.type ring.ringInst
-  let negFn ← mkUnaryFn ring.type ring.u ``Neg ``Neg.neg expectedInst
-  modifyRing fun s => { s with negFn? := some negFn }
-  return negFn
-
-def getPowFn : m Expr := do
-  let ring ← getRing
-  if let some powFn := ring.powFn? then return powFn
-  let powFn ← mkPowFn ring.u ring.type ring.semiringInst
-  modifyRing fun s => { s with powFn? := some powFn }
-  return powFn
-
-def getIntCastFn : m Expr := do
-  let ring ← getRing
-  if let some intCastFn := ring.intCastFn? then return intCastFn
-  let inst' := mkApp2 (mkConst ``Grind.Ring.intCast [ring.u]) ring.type ring.ringInst
-  let instType := mkApp (mkConst ``IntCast [ring.u]) ring.type
-  -- Note: `Ring.intCast` is not a global instance. Same pattern as `mkNatCastFn`.
-  let inst ← match (← MonadCanon.synthInstance? instType) with
-    | none => pure inst'
-    | some inst => checkInst ``Int.cast inst inst'; pure inst
-  let intCastFn ← canonExpr <| mkApp2 (mkConst ``IntCast.intCast [ring.u]) ring.type inst
-  modifyRing fun s => { s with intCastFn? := some intCastFn }
-  return intCastFn
-
-def getNatCastFn : m Expr := do
-  let ring ← getRing
-  if let some natCastFn := ring.natCastFn? then return natCastFn
-  let natCastFn ← mkNatCastFn ring.u ring.type ring.semiringInst
-  modifyRing fun s => { s with natCastFn? := some natCastFn }
-  return natCastFn
-
-end RingFns
-
-section CommRingFns
-variable [MonadCommRing m]
-
-def getInvFn : m Expr := do
-  let ring ← getCommRing
-  let some fieldInst := ring.fieldInst?
-    | throwError "internal error: type is not a field{indentExpr ring.type}"
-  if let some invFn := ring.invFn? then return invFn
-  let expectedInst := mkApp2 (mkConst ``Grind.Field.toInv [ring.u]) ring.type fieldInst
-  let invFn ← mkUnaryFn ring.type ring.u ``Inv ``Inv.inv expectedInst
-  modifyCommRing fun s => { s with invFn? := some invFn }
-  return invFn
-
-end CommRingFns
-
-section SemiringFns
-variable [MonadSemiring m]
-
-def getAddFn' : m Expr := do
-  let sr ← getSemiring
-  if let some addFn := sr.addFn? then return addFn
-  let expectedInst := mkApp2 (mkConst ``instHAdd [sr.u]) sr.type <| mkApp2 (mkConst ``Grind.Semiring.toAdd [sr.u]) sr.type sr.semiringInst
-  let addFn ← mkBinHomoFn sr.type sr.u ``HAdd ``HAdd.hAdd expectedInst
-  modifySemiring fun s => { s with addFn? := some addFn }
-  return addFn
-
-def getMulFn' : m Expr := do
-  let sr ← getSemiring
-  if let some mulFn := sr.mulFn? then return mulFn
-  let expectedInst := mkApp2 (mkConst ``instHMul [sr.u]) sr.type <| mkApp2 (mkConst ``Grind.Semiring.toMul [sr.u]) sr.type sr.semiringInst
-  let mulFn ← mkBinHomoFn sr.type sr.u ``HMul ``HMul.hMul expectedInst
-  modifySemiring fun s => { s with mulFn? := some mulFn }
-  return mulFn
-
-def getPowFn' : m Expr := do
-  let sr ← getSemiring
-  if let some powFn := sr.powFn? then return powFn
-  let powFn ← mkPowFn sr.u sr.type sr.semiringInst
-  modifySemiring fun s => { s with powFn? := some powFn }
-  return powFn
-
-def getNatCastFn' : m Expr := do
-  let sr ← getSemiring
-  if let some natCastFn := sr.natCastFn? then return natCastFn
-  let natCastFn ← mkNatCastFn sr.u sr.type sr.semiringInst
-  modifySemiring fun s => { s with natCastFn? := some natCastFn }
-  return natCastFn
-
-end SemiringFns
-
-end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/MonadRing.lean

@@ -1,39 +0,0 @@
-/-
-Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Sym.Arith.MonadCanon
-public section
-namespace Lean.Meta.Sym.Arith
-
-class MonadRing (m : Type → Type) where
-  getRing : m Ring
-  modifyRing : (Ring → Ring) → m Unit
-
-export MonadRing (getRing modifyRing)
-
-@[always_inline]
-instance (m n) [MonadLift m n] [MonadRing m] : MonadRing n where
-  getRing    := liftM (getRing : m Ring)
-  modifyRing f := liftM (modifyRing f : m Unit)
-
-class MonadCommRing (m : Type → Type) where
-  getCommRing : m CommRing
-  modifyCommRing : (CommRing → CommRing) → m Unit
-
-export MonadCommRing (getCommRing modifyCommRing)
-
-@[always_inline]
-instance (m n) [MonadLift m n] [MonadCommRing m] : MonadCommRing n where
-  getCommRing      := liftM (getCommRing : m CommRing)
-  modifyCommRing f := liftM (modifyCommRing f : m Unit)
-
-@[always_inline]
-instance (m) [Monad m] [MonadCommRing m] : MonadRing m where
-  getRing := return (← getCommRing).toRing
-  modifyRing f := modifyCommRing fun s => { s with toRing := f s.toRing }
-
-end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/MonadSemiring.lean

@@ -1,39 +0,0 @@
-/-
-Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Sym.Arith.MonadCanon
-public section
-namespace Lean.Meta.Sym.Arith
-
-class MonadSemiring (m : Type → Type) where
-  getSemiring : m Semiring
-  modifySemiring : (Semiring → Semiring) → m Unit
-
-export MonadSemiring (getSemiring modifySemiring)
-
-@[always_inline]
-instance (m n) [MonadLift m n] [MonadSemiring m] : MonadSemiring n where
-  getSemiring    := liftM (getSemiring : m Semiring)
-  modifySemiring f := liftM (modifySemiring f : m Unit)
-
-class MonadCommSemiring (m : Type → Type) where
-  getCommSemiring : m CommSemiring
-  modifyCommSemiring : (CommSemiring → CommSemiring) → m Unit
-
-export MonadCommSemiring (getCommSemiring modifyCommSemiring)
-
-@[always_inline]
-instance (m n) [MonadLift m n] [MonadCommSemiring m] : MonadCommSemiring n where
-  getCommSemiring      := liftM (getCommSemiring : m CommSemiring)
-  modifyCommSemiring f := liftM (modifyCommSemiring f : m Unit)
-
-@[always_inline]
-instance (m) [Monad m] [MonadCommSemiring m] : MonadSemiring m where
-  getSemiring := return (← getCommSemiring).toSemiring
-  modifySemiring f := modifyCommSemiring fun s => { s with toSemiring := f s.toSemiring }
-
-end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/MonadVar.lean

@@ -1,32 +0,0 @@
-/-
-Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Sym.Arith.Types
-public section
-namespace Lean.Meta.Sym.Arith
-
-/-- Read a variable's Lean expression by index. Used by `DenoteExpr` and diagnostics (PP). -/
-class MonadGetVar (m : Type → Type) where
-  getVar : Var → m Expr
-
-export MonadGetVar (getVar)
-
-@[always_inline]
-instance (m n) [MonadLift m n] [MonadGetVar m] : MonadGetVar n where
-  getVar x := liftM (getVar x : m Expr)
-
-/-- Create or lookup a variable for a Lean expression. Used by reification. -/
-class MonadMkVar (m : Type → Type) where
-  mkVar : Expr → m Var
-
-export MonadMkVar (mkVar)
-
-@[always_inline]
-instance (m n) [MonadLift m n] [MonadMkVar m] : MonadMkVar n where
-  mkVar e := liftM (mkVar e : m Var)
-
-end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/Reify.lean

@@ -1,205 +0,0 @@
-/-
-Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Sym.Arith.Functions
-public import Lean.Meta.Sym.Arith.MonadVar
-public import Lean.Meta.Sym.LitValues
-public section
-namespace Lean.Meta.Sym.Arith
-open Sym.Arith (MonadCanon)
-
-/-!
-# Reification of arithmetic expressions
-
-Converts Lean expressions into `CommRing.Expr` (ring) or `CommSemiring.Expr`
-(semiring) for reflection-based normalization.
-
-Instance validation uses pointer equality (`isSameExpr`) against cached function
-expressions from `Functions.lean`.
-
-## Differences from grind's `Reify.lean`
-
-- Uses `MonadMkVar` for variable creation instead of grind's `internalize` + `mkVarCore`
-- Uses `Sym.getNatValue?`/`Sym.getIntValue?` (pure) instead of `MetaM` versions
-- No `MonadSetTermId` — term-to-ring-id tracking is grind-specific
--/
-
-section RingReify
-
-variable [MonadLiftT SymM m] [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] [MonadMkVar m]
-
-def isAddInst (inst : Expr) : m Bool :=
-  return isSameExpr (← getAddFn).appArg! inst
-def isMulInst (inst : Expr) : m Bool :=
-  return isSameExpr (← getMulFn).appArg! inst
-def isSubInst (inst : Expr) : m Bool :=
-  return isSameExpr (← getSubFn).appArg! inst
-def isNegInst (inst : Expr) : m Bool :=
-  return isSameExpr (← getNegFn).appArg! inst
-def isPowInst (inst : Expr) : m Bool :=
-  return isSameExpr (← getPowFn).appArg! inst
-def isIntCastInst (inst : Expr) : m Bool :=
-  return isSameExpr (← getIntCastFn).appArg! inst
-def isNatCastInst (inst : Expr) : m Bool :=
-  return isSameExpr (← getNatCastFn).appArg! inst
-
-private def reportRingAppIssue [MonadLiftT SymM m] (e : Expr) : m Unit := do
-  reportIssue! "ring term with unexpected instance{indentExpr e}"
-
-/--
-Converts a Lean expression `e` into a `RingExpr`.
-
-If `skipVar` is `true`, returns `none` if `e` is not an interpreted ring term
-(used for equalities/disequalities). If `false`, treats non-interpreted terms
-as variables (used for inequalities).
--/
-partial def reifyRing? (e : Expr) (skipVar : Bool := true) : m (Option RingExpr) := do
-  let toVar (e : Expr) : m RingExpr := do
-    return .var (← mkVar e)
-  let asVar (e : Expr) : m RingExpr := do
-    reportRingAppIssue e
-    return .var (← mkVar e)
-  let rec go (e : Expr) : m RingExpr := do
-    match_expr e with
-    | HAdd.hAdd _ _ _ i a b =>
-      if (← isAddInst i) then return .add (← go a) (← go b) else asVar e
-    | HMul.hMul _ _ _ i a b =>
-      if (← isMulInst i) then return .mul (← go a) (← go b) else asVar e
-    | HSub.hSub _ _ _ i a b =>
-      if (← isSubInst i) then return .sub (← go a) (← go b) else asVar e
-    | HPow.hPow _ _ _ i a b =>
-      let some k := Sym.getNatValue? b |>.run | toVar e
-      if (← isPowInst i) then return .pow (← go a) k else asVar e
-    | Neg.neg _ i a =>
-      if (← isNegInst i) then return .neg (← go a) else asVar e
-    | IntCast.intCast _ i a =>
-      if (← isIntCastInst i) then
-        let some k := Sym.getIntValue? a |>.run | toVar e
-        return .intCast k
-      else
-        asVar e
-    | NatCast.natCast _ i a =>
-      if (← isNatCastInst i) then
-        let some k := Sym.getNatValue? a |>.run | toVar e
-        return .natCast k
-      else
-        asVar e
-    | OfNat.ofNat _ n _ =>
-      /-
-      **Note**: We extract `n` directly as a raw nat literal. The grind version uses `MetaM`'s
-      `getNatValue?` which handles multiple encodings (raw literals, nested `OfNat`, etc.).
-      In `SymM`, we assume terms have been canonicalized by `Sym.canon` before reification,
-      so `OfNat.ofNat _ n _` always has a raw nat literal at position 1.
-      -/
-      let .lit (.natVal k) := n | toVar e
-      return .num k
-    | BitVec.ofNat _ n =>
-      let .lit (.natVal k) := n | toVar e
-      return .num k
-    | _ => toVar e
-  let toTopVar (e : Expr) : m (Option RingExpr) := do
-    if skipVar then
-      return none
-    else
-      return some (← toVar e)
-  let asTopVar (e : Expr) : m (Option RingExpr) := do
-    reportRingAppIssue e
-    toTopVar e
-  match_expr e with
-  | HAdd.hAdd _ _ _ i a b =>
-    if (← isAddInst i) then return some (.add (← go a) (← go b)) else asTopVar e
-  | HMul.hMul _ _ _ i a b =>
-    if (← isMulInst i) then return some (.mul (← go a) (← go b)) else asTopVar e
-  | HSub.hSub _ _ _ i a b =>
-    if (← isSubInst i) then return some (.sub (← go a) (← go b)) else asTopVar e
-  | HPow.hPow _ _ _ i a b =>
-    let some k := Sym.getNatValue? b |>.run | asTopVar e
-    if (← isPowInst i) then return some (.pow (← go a) k) else asTopVar e
-  | Neg.neg _ i a =>
-    if (← isNegInst i) then return some (.neg (← go a)) else asTopVar e
-  | IntCast.intCast _ i a =>
-    if (← isIntCastInst i) then
-      let some k := Sym.getIntValue? a |>.run | toTopVar e
-      return some (.intCast k)
-    else
-      asTopVar e
-  | NatCast.natCast _ i a =>
-    if (← isNatCastInst i) then
-      let some k := Sym.getNatValue? a |>.run | toTopVar e
-      return some (.natCast k)
-    else
-      asTopVar e
-  | OfNat.ofNat _ n _ =>
-    let .lit (.natVal k) := n | asTopVar e
-    return some (.num k)
-  | _ => toTopVar e
-
-end RingReify
-
-section SemiringReify
-
-variable [MonadLiftT SymM m] [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadSemiring m] [MonadMkVar m]
-
-private def reportSemiringAppIssue [MonadLiftT SymM m] (e : Expr) : m Unit := do
-  reportIssue! "semiring term with unexpected instance{indentExpr e}"
-
-/--
-Converts a Lean expression `e` into a `SemiringExpr`.
-Only recognizes `add`, `mul`, `pow`, `natCast`, and numerals (no `sub`, `neg`, `intCast`).
--/
-partial def reifySemiring? (e : Expr) : m (Option SemiringExpr) := do
-  let toVar (e : Expr) : m SemiringExpr := do
-    return .var (← mkVar e)
-  let asVar (e : Expr) : m SemiringExpr := do
-    reportSemiringAppIssue e
-    return .var (← mkVar e)
-  let rec go (e : Expr) : m SemiringExpr := do
-    match_expr e with
-    | HAdd.hAdd _ _ _ i a b =>
-      if isSameExpr (← getAddFn').appArg! i then return .add (← go a) (← go b) else asVar e
-    | HMul.hMul _ _ _ i a b =>
-      if isSameExpr (← getMulFn').appArg! i then return .mul (← go a) (← go b) else asVar e
-    | HPow.hPow _ _ _ i a b =>
-      let some k := Sym.getNatValue? b |>.run | toVar e
-      if isSameExpr (← getPowFn').appArg! i then return .pow (← go a) k else asVar e
-    | NatCast.natCast _ i a =>
-      if isSameExpr (← getNatCastFn').appArg! i then
-        let some k := Sym.getNatValue? a |>.run | toVar e
-        return .num k
-      else
-        asVar e
-    | OfNat.ofNat _ n _ =>
-      let .lit (.natVal k) := n | toVar e
-      return .num k
-    | _ => toVar e
-  let toTopVar (e : Expr) : m (Option SemiringExpr) := do
-    return some (← toVar e)
-  let asTopVar (e : Expr) : m (Option SemiringExpr) := do
-    reportSemiringAppIssue e
-    toTopVar e
-  match_expr e with
-  | HAdd.hAdd _ _ _ i a b =>
-    if isSameExpr (← getAddFn').appArg! i then return some (.add (← go a) (← go b)) else asTopVar e
-  | HMul.hMul _ _ _ i a b =>
-    if isSameExpr (← getMulFn').appArg! i then return some (.mul (← go a) (← go b)) else asTopVar e
-  | HPow.hPow _ _ _ i a b =>
-    let some k := Sym.getNatValue? b |>.run | return none
-    if isSameExpr (← getPowFn').appArg! i then return some (.pow (← go a) k) else asTopVar e
-  | NatCast.natCast _ i a =>
-    if isSameExpr (← getNatCastFn').appArg! i then
-      let some k := Sym.getNatValue? a |>.run | toTopVar e
-      return some (.num k)
-    else
-      asTopVar e
-  | OfNat.ofNat _ n _ =>
-    let .lit (.natVal k) := n | asTopVar e
-    return some (.num k)
-  | _ => toTopVar e
-
-end SemiringReify
-
-end Lean.Meta.Sym.Arith

src/Lean/Meta/Sym/Arith/Types.lean

@@ -1,137 +0,0 @@
-/-
-Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Init.Grind.Ring.CommSemiringAdapter
-public import Lean.Meta.Sym.SymM
-public section
-
-namespace Lean.Meta.Sym.Arith
-export Lean.Grind.CommRing (Var Power Mon Poly)
-abbrev RingExpr := Grind.CommRing.Expr
-/-
-**Note**: recall that we use ring expressions to represent semiring expressions,
-and ignore non-applicable constructors.
--/
-abbrev SemiringExpr := Grind.CommRing.Expr
-
-/-- Classification state for a type with a `Semiring` instance. -/
-structure Semiring where
-  id             : Nat
-  type           : Expr
-  /-- Cached `getDecLevel type` -/
-  u              : Level
-  /-- `Semiring` instance for `type` -/
-  semiringInst   : Expr
-  addFn?         : Option Expr := none
-  mulFn?         : Option Expr := none
-  powFn?         : Option Expr := none
-  natCastFn?     : Option Expr := none
-  deriving Inhabited
-
-/-- Classification state for a type with a `Ring` instance. -/
-structure Ring where
-  id             : Nat
-  type           : Expr
-  /-- Cached `getDecLevel type` -/
-  u              : Level
-  /-- `Ring` instance for `type` -/
-  ringInst       : Expr
-  /-- `Semiring` instance for `type` -/
-  semiringInst   : Expr
-  /-- `IsCharP` instance for `type` if available. -/
-  charInst?      : Option (Expr × Nat)
-  addFn?         : Option Expr := none
-  mulFn?         : Option Expr := none
-  subFn?         : Option Expr := none
-  negFn?         : Option Expr := none
-  powFn?         : Option Expr := none
-  intCastFn?     : Option Expr := none
-  natCastFn?     : Option Expr := none
-  one?           : Option Expr := none
-  deriving Inhabited
-
-/-- Classification state for a type with a `CommRing` instance. -/
-structure CommRing extends Ring where
-  /-- Inverse function if `fieldInst?` is `some inst` -/
-  invFn?             : Option Expr := none
-  /--
-  If this is a `OfSemiring.Q α` ring, this field contains the
-  `semiringId` for `α`.
-  -/
-  semiringId?        : Option Nat
-  /-- `CommSemiring` instance for `type` -/
-  commSemiringInst   : Expr
-  /-- `CommRing` instance for `type` -/
-  commRingInst       : Expr
-  /-- `NoNatZeroDivisors` instance for `type` if available. -/
-  noZeroDivInst?     : Option Expr
-  /-- `Field` instance for `type` if available. -/
-  fieldInst?         : Option Expr
-  deriving Inhabited
-
-/--
-Classification state for a type with a `CommSemiring` instance.
-Recall that `CommSemiring` types are normalized using the `OfSemiring.Q` envelope.
--/
-structure CommSemiring extends Semiring where
-  /-- Id of the envelope ring `OfSemiring.Q type` -/
-  ringId             : Nat
-  /-- `CommSemiring` instance for `type` -/
-  commSemiringInst   : Expr
-  /-- `AddRightCancel` instance for `type` if available. -/
-  addRightCancelInst? : Option (Option Expr) := none
-  toQFn?             : Option Expr := none
-  deriving Inhabited
-
-/-- Result of classifying a type's algebraic structure. -/
-inductive ClassifyResult where
-  | commRing (id : Nat)
-  | nonCommRing (id : Nat)
-  | commSemiring (id : Nat)
-  | nonCommSemiring (id : Nat)
-  | /-- No algebraic structure found. -/ none
-  deriving Inhabited
-
-/-- Arith type classification state, stored as a `SymExtension`. -/
-structure State where
-  /-- Exponent threshold for `HPow` evaluation. -/
-  exp            : Nat := 8
-  /-- Commutative rings. -/
-  rings          : Array CommRing := {}
-  /-- Commutative semirings. -/
-  semirings      : Array CommSemiring := {}
-  /-- Non-commutative rings. -/
-  ncRings        : Array Ring := {}
-  /-- Non-commutative semirings. -/
-  ncSemirings    : Array Semiring := {}
-  /-- Mapping from types to their classification result. Caches failures as `.none`. -/
-  typeClassify   : PHashMap ExprPtr ClassifyResult := {}
-  deriving Inhabited
-
-builtin_initialize arithExt : SymExtension State ← registerSymExtension (return {})
-
-def getArithState : SymM State :=
-  arithExt.getState
-
-@[inline] def modifyArithState (f : State → State) : SymM Unit :=
-  arithExt.modifyState f
-
-/-- Get the exponent threshold. -/
-def getExpThreshold : SymM Nat :=
-  return (← getArithState).exp
-
-/-- Set the exponent threshold. -/
-def setExpThreshold (exp : Nat) : SymM Unit :=
-  modifyArithState fun s => { s with exp }
-
-/-- Run `k` with a temporary exponent threshold. -/
-def withExpThreshold (exp : Nat) (k : SymM α) : SymM α := do
-  let oldExp := (← getArithState).exp
-  setExpThreshold exp
-  try k finally setExpThreshold oldExp
-
-end Lean.Meta.Sym.Arith

src/Lean/Meta/Tactic/Grind/Arith/CommRing.lean

@@ -5,9 +5,11 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Internalize
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.SemiringM
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommRingM
@@ -19,6 +21,8 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Inv
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.PP
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadCanon
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadSemiring
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Action

src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean

@@ -8,7 +8,6 @@ prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith
 /-!
 Helper functions for converting reified terms back into their denotations.
 -/

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Functions.lean

@@ -8,7 +8,6 @@ prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith
 variable [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m]
 
 section

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Inv.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
-import Lean.Meta.Sym.Arith.Poly
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 

src/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadCanon.lean

@@ -1,23 +1,24 @@
 /-
-Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Sym.Arith.Types
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
 public section
-namespace Lean.Meta.Sym.Arith
+namespace Lean.Meta.Grind.Arith.CommRing
 
 class MonadCanon (m : Type → Type) where
   /--
-  Canonicalize an expression (types, instances, support arguments).
-  In `SymM`, this is `Sym.canon`. In `PP.M` (diagnostics), this is the identity.
+  Helper function for removing dependency on `GoalM`.
+  In `RingM` and `SemiringM`, this is just `sharedCommon (← canon e)`
+  When printing counterexamples, we are at `MetaM`, and this is just the identity function.
   -/
   canonExpr : Expr → m Expr
   /--
-  Synthesize an instance, returning `none` on failure.
-  In `SymM`, this is `Sym.synthInstance?`. In `PP.M`, this is `Meta.synthInstance?`.
+  Helper function for removing dependency on `GoalM`. During search we
+  want to track the instances synthesized by `grind`, and this is `Grind.synthInstance`.
   -/
   synthInstance? : Expr → m (Option Expr)
 
@@ -30,7 +31,7 @@ instance (m n) [MonadLift m n] [MonadCanon m] : MonadCanon n where
 
 def MonadCanon.synthInstance [Monad m] [MonadError m] [MonadCanon m] (type : Expr) : m Expr := do
   let some inst ← synthInstance? type
-    | throwError "failed to find instance{indentExpr type}"
+    | throwError "`grind` failed to find instance{indentExpr type}"
   return inst
 
-end Lean.Meta.Sym.Arith
+end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadRing.lean

@@ -5,8 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Sym.Arith.MonadCanon
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadCanon
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 

src/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadSemiring.lean

@@ -5,8 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Sym.Arith.MonadCanon
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadCanon
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
 

src/Lean/Meta/Tactic/Grind/Arith/CommRing/NonCommRingM.lean

@@ -8,7 +8,7 @@ prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith
+
 structure NonCommRingM.Context where
   ringId : Nat
 

src/Lean/Meta/Tactic/Grind/Arith/CommRing/NonCommSemiringM.lean

@@ -8,7 +8,6 @@ prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.SemiringM
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith (MonadCanon)
 
 structure NonCommSemiringM.Context where
   semiringId : Nat

src/Lean/Meta/Tactic/Grind/Arith/CommRing/PP.lean

@@ -10,7 +10,6 @@ import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 import Init.Omega
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith
 
 private abbrev M := StateT CommRing MetaM
 

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean

@@ -12,14 +12,12 @@ import Lean.Data.RArray
 import Lean.Meta.Tactic.Grind.Diseq
 import Lean.Meta.Tactic.Grind.ProofUtil
 import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
-import Lean.Meta.Sym.Arith.ToExpr
-import Lean.Meta.Sym.Arith.VarRename
+import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
+import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename
 import Init.Data.Nat.Order
 import Init.Data.Order.Lemmas
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith (MonadCanon)
-
 /--
 Returns a context of type `RArray α` containing the variables `vars` where
 `α` is the type of the ring.

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Reify.lean

@@ -9,7 +9,6 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommRingM
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommSemiringM
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith (MonadCanon)
 
 variable [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m]
 

src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingM.lean

@@ -9,7 +9,6 @@ public import Lean.Meta.Tactic.Grind.SynthInstance
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith
 
 def checkMaxSteps : GoalM Bool := do
   return (← get').steps >= (← getConfig).ringSteps

src/Lean/Meta/Tactic/Grind/Arith/CommRing/SafePoly.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
-public import Lean.Meta.Sym.Arith.Poly
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 import Lean.Meta.Tactic.Grind.Arith.EvalNum
 import Init.Data.Nat.Linear
 public section

src/Lean/Meta/Tactic/Grind/Arith/CommRing/SemiringM.lean

@@ -11,7 +11,6 @@ import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-open Sym.Arith
 
 structure SemiringM.Context where
   semiringId : Nat

src/Lean/Meta/Tactic/Grind/Arith/CommRing/ToExpr.lean

@@ -8,7 +8,7 @@ prelude
 public import Init.Grind.Ring.CommSemiringAdapter
 public import Lean.ToExpr
 public section
-namespace Lean.Meta.Sym.Arith
+namespace Lean.Meta.Grind.Arith.CommRing
 open Grind.CommRing
 /-!
 `ToExpr` instances for `CommRing.Poly` types.
@@ -57,4 +57,4 @@ instance : ToExpr CommRing.Expr where
   toExpr := ofRingExpr
   toTypeExpr := mkConst ``CommRing.Expr
 
-end Lean.Meta.Sym.Arith
+end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean

@@ -7,7 +7,7 @@ module
 prelude
 public import Init.Grind.Ring.CommSemiringAdapter
 public import Lean.Meta.Tactic.Grind.Types
-import Lean.Meta.Sym.Arith.Poly
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 public section
 
 namespace Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean

@@ -14,8 +14,8 @@ import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.VarRename
-import Lean.Meta.Sym.Arith.VarRename
-import Lean.Meta.Sym.Arith.ToExpr
+import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename
+import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
 import Init.Data.Nat.Order
 import Init.Data.Order.Lemmas
 public section

src/Lean/Meta/Tactic/Grind/Arith/Linear/LinearM.lean

@@ -9,7 +9,6 @@ public import Lean.Meta.Tactic.Grind.Arith.Linear.Types
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 public section
 namespace Lean.Meta.Grind.Arith.Linear
-open Sym.Arith (MonadCanon)
 
 def get' : GoalM State := do
   linearExt.getState

src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean

@@ -11,8 +11,8 @@ import Lean.Data.RArray
 import Lean.Meta.Tactic.Grind.Arith.Linear.ToExpr
 import Lean.Meta.Tactic.Grind.Diseq
 import Lean.Meta.Tactic.Grind.ProofUtil
-import Lean.Meta.Sym.Arith.VarRename
-import Lean.Meta.Sym.Arith.ToExpr
+import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename
+import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
 import Lean.Meta.Tactic.Grind.Arith.Linear.VarRename
 public import Lean.Meta.Tactic.Grind.Arith.Linear.DenoteExpr
 public import Lean.Meta.Tactic.Grind.Arith.Linear.OfNatModule

src/Lean/Meta/Tactic/Grind/Order/Internalize.lean

@@ -97,8 +97,6 @@ def mkCnstrNorm0 (s : Struct) (ringInst : Expr) (kind : CnstrKind) (lhs rhs : Ex
   | .le => mkLeNorm0 s ringInst lhs rhs
   | .lt => mkLtNorm0 s ringInst lhs rhs
 
-open Sym.Arith (MonadCanon)
-
 /--
 Returns `rel lhs (rhs + 0)`
 -/

src/Lean/Server/Logging.lean

@@ -90,11 +90,11 @@ where
     messageMethod? msg <|> (do pending.get? (← messageId? msg))
 
 local instance : ToJson Std.Time.ZonedDateTime where
-  toJson dt := dt.toISO8601String
+  toJson dt := Std.Time.Formats.iso8601.format dt
 
 local instance : FromJson Std.Time.ZonedDateTime where
   fromJson?
-    | .str s => Std.Time.ZonedDateTime.fromISO8601String s
+    | .str s => Std.Time.Formats.iso8601.parse s
     | _ => throw "Expected string when converting JSON to Std.Time.ZonedDateTime"
 
 structure LogEntry where

src/Std/Time.lean

@@ -17,8 +17,7 @@ public import Std.Time.Zoned.Database
 
 public section
 
-namespace Std
-namespace Time
+namespace Std.Time
 
 /-!
 # Time
@@ -130,23 +129,30 @@ Represents spans of time and the difference between two points in time.
 # 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 table below shows the available format specifiers. Repeating a pattern character may change the
+text style, minimum width, or offset/fraction form, depending on the field.
 
-The `number` type format specifiers, such as `h` and `K`, are parsed based on the number of repetitions.
-If the repetition count is one, the format allows values ranging from 1 up to the maximum capacity of
-the respective data type.
+The current Lean implementation follows Java's pattern language where practical, but it is not fully
+locale-sensitive. Text forms currently use English data, and localized weekday/week-of-month fields use
+the library's fixed Monday-first interpretation.
+
+For numeric fields that accept both one- and two-letter forms, the single-letter form parses a
+non-padded number and the two-letter form parses a zero-padded width of two.
 
 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").
+- `G`: Represents the era, such as BCE (Before Common Era) or CE (Common Era).
+  - `G`, `GG`, `GGG` (short): Displays the era in a short format (e.g., "CE").
+  - `GGGG` (full): Displays the era in a full format (e.g., "Common Era").
+  - `GGGGG` (narrow): Displays the era in a narrow format (e.g., "C").
 - `y`: Represents the year of the era.
   - `y`: Represents the year in its full form, without a fixed length. It can handle years of any size, (e.g., "1", "2025", or "12345678").
   - `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.
+- `Y`: Represents the week-based year (ISO-like behavior around year boundaries).
+  - `Y`, `YYY`, `YYYY`: Displays the week-based year (e.g., "2017").
+  - `YY`: Displays the last two digits of the week-based year (e.g., "17").
+  - `YYYYY+`: Extended format for week-based years with more than four digits.
 - `u`: Represents the year.
   - `u`: Represents the year in its full form, without a fixed length. It can handle years of any size, (e.g., "1", "2025", or "12345678").
   - `uu`: Two-digit year format, showing the last two digits (e.g., "04" for 2004).
@@ -158,69 +164,94 @@ The supported formats include:
   - `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).
+- `L`: Represents the standalone month of the year.
+  - Supports the same widths as `M`; in the current English data it formats the same values.
 - `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").
+- `q`: Represents the standalone quarter of the year.
+  - Supports the same widths as `Q`; in the current English data it formats the same values.
 - `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").
+- `W`: Represents the week of the month using the library's fixed Monday-first week model (e.g., "2").
 - `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).
+  - `EEEEEE`: Displays the short two-letter weekday name (e.g., "Tu").
 - `e`: Represents the weekday as number or text.
   - `e`, `ee`: Displays the weekday 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").
+  - `eeeeee`: Displays the short two-letter weekday name (e.g., "Tu").
+- `c`: Standalone weekday.
+  - `c`: Displays the numeric weekday using the same Monday-to-Sunday numbering as `e`.
+  - `ccc`, `cccc`, `ccccc`: Display standalone text (same values as `e` in the current English data).
+  - `cccccc`: Displays the short two-letter weekday name (e.g., "Tu").
+- `F`: Represents the occurrence of the weekday within the month (e.g., the 2nd Sunday formats as `2`).
 - `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").
+  - `a`, `aa`, `aaa`: Displays AM/PM (e.g., "PM").
+  - `aaaa`: Displays the full form (e.g., "ante meridiem", "post meridiem").
+  - `aaaaa`: Displays the narrow form (e.g., "a", "p").
+- `b`: Represents the day period, extending AM/PM with noon and midnight (TR35 §4, supported in Java 16+). The `B` symbol (flexible day periods) is not supported.
+  - `b`, `bb`, `bbb`: Displays a short form (e.g., "AM", "PM", "noon", "midnight").
+  - `bbbb`: Displays a full form (e.g., "ante meridiem", "post meridiem", "noon", "midnight"); unlike `a`, the AM/PM spellings are lowercase here.
+  - `bbbbb`: Displays a narrow form (e.g., "a", "p", "n", "mi").
 - `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.
+  - `h`, `hh` are supported, matching Java.
 - `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`, `KK` are supported, matching Java.
 - `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.
+  - `k`, `kk` are supported, matching Java.
 - `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.
+  - `H`, `HH` are supported, matching Java.
 - `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.
+  - `m`, `mm` are supported, matching Java.
 - `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`, `ss` are supported, matching Java.
 - `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.
+  - One or more repetitions of the character truncates to the specified number of most-significant digits; it does not round.
 - `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.
+  - One or more repetitions of the character indicates zero-padding to the specified number of characters (no truncation is applied).
+- `n`: Represents the nanosecond of the second (e.g., "987654321"). This is a Lean/Java extension, not a TR35 field.
+  - One or more repetitions of the character sets a minimum width via zero-padding; the value is not truncated.
+- `N`: Represents the nanosecond of the day (e.g., "1234000000"). This is a Lean/Java extension, not a TR35 field.
+  - One or more repetitions of the character sets a minimum width via zero-padding; the value is not truncated.
+- `V`: Time zone ID.
+  - `VV`: Displays the zone identifier/name.
+  - Other counts are unsupported, matching Java.
 - `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").
+  - `z`, `zz`, `zzz`: Shows a short zone name; for offset-only zones this is the numeric offset (e.g., "+09:00"), for UTC this is "UTC", otherwise the abbreviation (e.g., "PST").
+  - `zzzz`: Displays the full zone name; for offset-only zones this is the numeric offset (e.g., "+09:00"), for UTC this is "Coordinated Universal Time", otherwise the full zone name (e.g., "Pacific Standard Time").
+- `v`: Generic time zone name.
+  - `v`: In the current Lean timezone data this displays the stored abbreviation; for offset-only zones this is the numeric offset (e.g., "+09:00"), and for UTC it is normalized to "UTC".
+  - `vvvv`: In the current Lean timezone data this displays the stored zone name/ID; for offset-only zones this is the numeric offset (e.g., "+09:00"), and for UTC it is normalized to "Coordinated Universal 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").
+  - `O`: Displays the GMT offset in a short format (e.g., "GMT+8"), or "GMT" for UTC.
+  - `OOOO`: Displays the full GMT offset with padded hour and minutes (e.g., "GMT+08:00"), or "GMT" for UTC.
 - `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").
+  - `X`: Displays hour and optional minute offset (e.g., "-08", "-0830", or "Z").
   - `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").
+  - `XXXX`: Displays the hour and minute offset without a colon, with optional seconds (e.g., "-0830", "-083045").
+  - `XXXXX`: Displays the hour and minute offset with a colon, with optional seconds (e.g., "-08:30", "-08:30:45").
+- `x`: Represents the zone offset. Similar to `X`, but never displays `'Z'` for UTC.
+  - `x`: Displays hour and optional minute offset (e.g., "+00", "+0530").
   - `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").
+  - `xxxx`: Displays the hour and minute offset without a colon, with optional seconds (e.g., "+0830", "+083045").
+  - `xxxxx`: Displays the hour and minute offset with a colon, with optional seconds (e.g., "+08:30", "+08:30:45").
+- `Z`: Represents the zone offset in RFC/CLDR `Z` forms.
+  - `Z`, `ZZ`, `ZZZ`: Displays hour and minute offset without colon, with optional seconds (e.g., "+0800", "+083045").
+  - `ZZZZ`: Displays localized GMT form (e.g., "GMT+08:00").
+  - `ZZZZZ`: Displays hour and minute offset with a colon and optional seconds, and uses `"Z"` for UTC (e.g., "Z", "+08:30", "+08:30:45").
+# Runtime Parsing
+
+- `ZonedDateTime.parse` parses common zoned date-time formats with explicit offsets, but does not resolve timezone identifiers like `[Europe/Paris]`.
+- `ZonedDateTime.parseIO` resolves identifier-based inputs via the default timezone database.
+- `ZonedDateTime.fromLeanDateTimeWithIdentifierString` is pure and does not perform timezone database resolution.
+- `ZonedDateTime.fromLeanDateTimeWithIdentifierStringIO` resolves identifiers using the default timezone database.
 
 # Macros
 
@@ -234,8 +265,10 @@ The `.sssssssss` can be omitted in most cases.
 - **`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.sssssssssZZZZZ")`**: 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.
 
 -/
+
+end Std.Time

src/Std/Time/Date/PlainDate.lean

@@ -355,6 +355,28 @@ def weekOfYear (date : PlainDate) : Week.Ordinal :=
     let w := w.truncateBottom h |>.truncateTop (Int.le_trans h₁ y.weeks.property.right)
     w
 
+/--
+Returns the week-based year for a given `PlainDate`.
+-/
+def weekBasedYear (date : PlainDate) : Year.Offset :=
+  let year := date.year
+  let doy  := date.dayOfYear
+  let dow  := date.weekday.toOrdinal.sub 1
+
+  if doy.val ≤ 3 then
+    if doy.val - dow.val < -2 then
+      year - 1
+    else
+      year
+  else if doy.val ≥ 363 then
+    let leap := if date.inLeapYear then 1 else 0
+    if (doy.val - 363 - leap) - dow.val ≥ 0 then
+      year + 1
+    else
+      year
+  else
+    year
+
 instance : HAdd PlainDate Day.Offset PlainDate where
   hAdd := addDays
 

src/Std/Time/DateTime/PlainDateTime.lean

@@ -502,6 +502,11 @@ def weekOfMonth (date : PlainDateTime) : Bounded.LE 1 5 :=
   date.date.weekOfMonth
 
 /--
+Returns the week-based year for a given `PlainDateTime`.
+-/
+def weekBasedYear (date : PlainDateTime) : Year.Offset :=
+  date.date.weekBasedYear
+/--
 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.

src/Std/Time/Format.lean

@@ -23,144 +23,207 @@ set_option linter.all true
 The ISO 8601 format, used for representing date and time in a standardized
 format. The format follows the pattern `uuuu-MM-dd'T'HH:mm:ssXXX`.
 -/
-def iso8601 : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ssXXX")
-
+def iso8601 : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ssXXX")
 
 /--
 The americanDate format, which follows the pattern `MM-dd-uuuu`.
 -/
-def americanDate : GenericFormat .any := datespec("MM-dd-uuuu")
+def americanDate : Format Awareness.any := datespec("MM-dd-uuuu")
 
 /--
 The europeanDate format, which follows the pattern `dd-MM-uuuu`.
 -/
-def europeanDate : GenericFormat .any := datespec("dd-MM-uuuu")
+def europeanDate : Format Awareness.any := datespec("dd-MM-uuuu")
 
 /--
-The time12Hour format, which follows the pattern `hh:mm:ss aa` for representing time
+The time12Hour format, which follows the pattern `hh:mm:ss a` for representing time
 in a 12-hour clock format with an upper case AM/PM marker.
 -/
-def time12Hour : GenericFormat .any := datespec("hh:mm:ss aa")
+def time12Hour : Format Awareness.any := datespec("hh:mm:ss a")
 
 /--
 The Time24Hour format, which follows the pattern `HH:mm:ss` for representing time
 in a 24-hour clock format.
 -/
-def time24Hour : GenericFormat .any := datespec("HH:mm:ss")
+def time24Hour : Format Awareness.any := datespec("HH:mm:ss")
 
 /--
 The DateTimeZone24Hour format, which follows the pattern `uuuu-MM-dd:HH:mm:ss.SSSSSSSSS` for
 representing date, time, and time zone.
 -/
-def dateTime24Hour : GenericFormat (.only .GMT) := datespec("uuuu-MM-dd:HH:mm:ss.SSSSSSSSS")
+def dateTime24Hour : Format (.only .GMT) := datespec("uuuu-MM-dd:HH:mm:ss.SSSSSSSSS")
 
 /--
 The DateTimeWithZone format, which follows the pattern `uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZ`
 for representing date, time, and time zone.
 -/
-def dateTimeWithZone : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZ")
+def dateTimeWithZone : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZ")
 
 /--
 The leanTime24Hour format, which follows the pattern `HH:mm:ss.SSSSSSSSS` for representing time
 in a 24-hour clock format. It uses the default value that can be parsed with the
 notation of dates.
 -/
-def leanTime24Hour : GenericFormat .any := datespec("HH:mm:ss.SSSSSSSSS")
+def leanTime24Hour : Format Awareness.any := datespec("HH:mm:ss.SSSSSSSSS")
 
 /--
 The leanTime24HourNoNanos format, which follows the pattern `HH:mm:ss` for representing time
 in a 24-hour clock format. It uses the default value that can be parsed with the
 notation of dates.
 -/
-def leanTime24HourNoNanos : GenericFormat .any := datespec("HH:mm:ss")
+def leanTime24HourNoNanos : Format Awareness.any := datespec("HH:mm:ss")
 
 /--
 The leanDateTime24Hour format, which follows the pattern `uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSS` for
 representing date, time, and time zone. It uses the default value that can be parsed with the
 notation of dates.
 -/
-def leanDateTime24Hour : GenericFormat (.only .GMT) := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSS")
+def leanDateTime24Hour : Format (.only .GMT) := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSS")
 
 /--
 The leanDateTime24HourNoNanos format, which follows the pattern `uuuu-MM-dd'T'HH:mm:ss` for
 representing date, time, and time zone. It uses the default value that can be parsed with the
 notation of dates.
 -/
-def leanDateTime24HourNoNanos : GenericFormat (.only .GMT) := datespec("uuuu-MM-dd'T'HH:mm:ss")
+def leanDateTime24HourNoNanos : Format (.only .GMT) := datespec("uuuu-MM-dd'T'HH:mm:ss")
 
 /--
 The leanDateTimeWithZone format, which follows the pattern `uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ`
 for representing date, time, and time zone. It uses the default value that can be parsed with the
 notation of dates.
 -/
-def leanDateTimeWithZone : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ")
+def leanDateTimeWithZone : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ")
 
 /--
 The leanDateTimeWithZoneNoNanos format, which follows the pattern `uuuu-MM-dd'T'HH:mm:ssZZZZZ`
 for representing date, time, and time zone. It uses the default value that can be parsed with the
 notation of dates.
 -/
-def leanDateTimeWithZoneNoNanos : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ssZZZZZ")
+def leanDateTimeWithZoneNoNanos : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ssZZZZZ")
 
 /--
 The leanDateTimeWithIdentifier format, which follows the pattern `uuuu-MM-dd'T'HH:mm:ss[z]`
 for representing date, time, and time zone. It uses the default value that can be parsed with the
 notation of dates.
 -/
-def leanDateTimeWithIdentifier : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss'['zzzz']'")
+def leanDateTimeWithIdentifier : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss'['VV']'")
 
 /--
 The leanDateTimeWithIdentifierAndNanos format, which follows the pattern `uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSS'[z]'`
 for representing date, time, and time zone. It uses the default value that can be parsed with the
 notation of dates.
 -/
-def leanDateTimeWithIdentifierAndNanos : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSS'['zzzz']'")
+def leanDateTimeWithIdentifierAndNanos : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSS'['VV']'")
+
+/--
+The leanDateTimeWithZoneAndName format, which follows the pattern
+`uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ'['VV']'` for representing date, time, timezone offset,
+and timezone identifier. This is the canonical Lean format used in `repr` for named timezones.
+-/
+def leanDateTimeWithZoneAndName : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ'['VV']'")
+
+/--
+The leanDateTimeWithZoneAndNameNoNanos format, which follows the pattern
+`uuuu-MM-dd'T'HH:mm:ssZZZZZ'['zzzz']'` for representing date, time, timezone offset, and timezone
+identifier without nanoseconds.
+-/
+def leanDateTimeWithZoneAndNameNoNanos : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ssZZZZZ'['VV']'")
 
 /--
 The Lean Date format, which follows the pattern `uuuu-MM-dd`. It uses the default value that can be parsed with the
 notation of dates.
 -/
-def leanDate : GenericFormat .any := datespec("uuuu-MM-dd")
+def leanDate : Format Awareness.any := datespec("uuuu-MM-dd")
 
 /--
 The SQLDate format, which follows the pattern `uuuu-MM-dd` and is commonly used
 in SQL databases to represent dates.
 -/
-def sqlDate : GenericFormat .any := datespec("uuuu-MM-dd")
+def sqlDate : Format Awareness.any := datespec("uuuu-MM-dd")
 
 /--
 The LongDateFormat, which follows the pattern `EEEE, MMMM d, uuuu HH:mm:ss` for
 representing a full date and time with the day of the week and month name.
 -/
-def longDateFormat : GenericFormat (.only .GMT) := datespec("EEEE, MMMM d, uuuu HH:mm:ss")
+def longDateFormat : Format (.only .GMT) := datespec("EEEE, MMMM d, uuuu HH:mm:ss")
 
 /--
 The AscTime format, which follows the pattern `EEE MMM d HH:mm:ss uuuu`. This format
 is often used in older systems for logging and time-stamping events.
 -/
-def ascTime : GenericFormat (.only .GMT) := datespec("EEE MMM d HH:mm:ss uuuu")
+def ascTime : Format (.only .GMT) := datespec("EEE MMM d HH:mm:ss uuuu")
 
 /--
 The RFC822 format, which follows the pattern `eee, dd MMM uuuu HH:mm:ss ZZZ`.
 This format is used in email headers and HTTP headers.
 -/
-def rfc822 : GenericFormat .any := datespec("eee, dd MMM uuuu HH:mm:ss ZZZ")
+def rfc822 : Format Awareness.any := datespec("eee, dd MMM uuuu HH:mm:ss ZZZ")
 
 /--
-The RFC850 format, which follows the pattern `eee, dd-MMM-YY HH:mm:ss ZZZ`.
+The RFC850 format, which follows the pattern `eee, dd-MMM-yy HH:mm:ss ZZZ`.
 This format is an older standard for representing date and time in headers.
 -/
-def rfc850 : GenericFormat .any := datespec("eee, dd-MM-uuuu HH:mm:ss ZZZ")
+def rfc850 : Format Awareness.any := datespec("eee, dd-MMM-yy HH:mm:ss ZZZ")
+
+/--
+A `MultiFormat` that parses `leanDateTimeWithZone` with or without nanoseconds.
+-/
+def leanDateTimeWithZoneAlt : MultiFormat Awareness.any :=
+  .new #[leanDateTimeWithZone, leanDateTimeWithZoneNoNanos]
+
+/--
+A `MultiFormat` that parses `leanDateTimeWithZoneAndName` with or without nanoseconds.
+-/
+def leanDateTimeWithZoneAndNameAlt : MultiFormat Awareness.any :=
+  .new #[leanDateTimeWithZoneAndName, leanDateTimeWithZoneAndNameNoNanos]
+
+/--
+A `MultiFormat` that parses `leanDateTime24Hour` with or without nanoseconds.
+-/
+def leanDateTime24HourAlt : MultiFormat (.only .GMT) :=
+  .new #[leanDateTime24Hour, leanDateTime24HourNoNanos]
+
+/--
+A `MultiFormat` that parses `leanTime24Hour` with or without nanoseconds.
+-/
+def leanTime24HourAlt : MultiFormat Awareness.any :=
+  .new #[leanTime24Hour, leanTime24HourNoNanos]
+
+/--
+A `MultiFormat` that parses `leanDateTimeWithIdentifier` with or without nanoseconds.
+-/
+def leanDateTimeWithIdentifierAlt : MultiFormat Awareness.any :=
+  .new #[leanDateTimeWithIdentifier, leanDateTimeWithIdentifierAndNanos]
 
 end Formats
 
+namespace Format
+
+/--
+Parses the input string, resolving any timezone identifier via the default timezone database.
+For formats with a timezone identifier specifier but no offset specifier (e.g.
+`uuuu-MM-dd'T'HH:mm:ss'['zzzz']'`), this performs a tzdb lookup to find the correct UTC offset.
+For all other formats this behaves identically to `parse`.
+-/
+def parseIO (format : Format Awareness.any) (input : String) : IO ZonedDateTime := do
+  if format.hasIdentifierSpecifier && !format.hasOffsetSpecifier then
+    match format.parseUnchecked input with
+    | .error err => throw <| IO.userError err
+    | .ok zdt =>
+      let rules ← Database.defaultGetZoneRules zdt.timezone.name
+      pure <| ZonedDateTime.ofPlainDateTime zdt.toPlainDateTime rules
+  else
+    IO.ofExcept (format.parse input)
+
+end Format
+
 namespace TimeZone
 
 /--
 Parses a string into a `TimeZone` object. The input string must be in the format `"VV ZZZZZ"`.
 -/
 def fromTimeZone (input : String) : Except String TimeZone := do
-  let spec : GenericFormat .any := datespec("VV ZZZZZ")
+  let spec : Format Awareness.any := datespec("VV ZZZZZ")
   spec.parseBuilder (fun id off => some (TimeZone.mk off id (off.toIsoString true) false)) input
 
 namespace Offset
@@ -169,7 +232,7 @@ namespace Offset
 Parses a string representing an offset into an `Offset` object. The input string must follow the `"xxx"` format.
 -/
 def fromOffset (input : String) : Except String Offset := do
-  let spec : GenericFormat .any := datespec("xxx")
+  let spec : Format Awareness.any := datespec("xxx")
   spec.parseBuilder some input
 
 end Offset
@@ -181,76 +244,44 @@ namespace PlainDate
 Formats a `PlainDate` using a specific format.
 -/
 def format (date : PlainDate) (format : String) : String :=
-  let format : Except String (GenericFormat .any) := GenericFormat.spec format
+  let format : Except String (Format Awareness.any) := Format.spec format
   match format with
   | .error err => s!"error: {err}"
   | .ok res =>
     let res := res.formatGeneric fun
       | .G _ => some date.era
       | .y _ => some date.year
+      | .Y _ => some date.weekBasedYear
       | .u _ => some date.year
       | .D _ => some (Sigma.mk date.year.isLeap date.dayOfYear)
-      | .Qorq _ => some date.quarter
+      | .Q _ | .q _ => some date.quarter
       | .w _ => some date.weekOfYear
-      | .W _ => some date.alignedWeekOfMonth
-      | .MorL _ => some date.month
+      | .W _ => some date.weekOfMonth
+      | .M _ | .L _ => some date.month
       | .d _ => some date.day
       | .E _ => some date.weekday
-      | .eorc _ => some date.weekday
+      | .e _ | .c _ => some date.weekday
       | .F _ => some date.weekOfMonth
       | _ => none
     match res with
     | some res => res
     | none => "invalid time"
 
-/--
-Parses a date string in the American format (`MM-dd-uuuu`) and returns a `PlainDate`.
--/
-def fromAmericanDateString (input : String) : Except String PlainDate := do
-  Formats.americanDate.parseBuilder (fun m d y => PlainDate.ofYearMonthDay? y m d) input
-
-/--
-Converts a date in the American format (`MM-dd-uuuu`) into a `String`.
--/
-def toAmericanDateString (input : PlainDate) : String :=
-  Formats.americanDate.formatBuilder input.month input.day input.year
-
-/--
-Parses a date string in the SQL format (`uuuu-MM-dd`) and returns a `PlainDate`.
--/
-def fromSQLDateString (input : String) : Except String PlainDate := do
-  Formats.sqlDate.parseBuilder PlainDate.ofYearMonthDay? input
-
-/--
-Converts a date in the SQL format (`uuuu-MM-dd`) into a `String`.
--/
-def toSQLDateString (input : PlainDate) : String :=
-  Formats.sqlDate.formatBuilder input.year input.month input.day
-
-/--
-Parses a date string in the Lean format (`uuuu-MM-dd`) and returns a `PlainDate`.
--/
-def fromLeanDateString (input : String) : Except String PlainDate := do
-  Formats.leanDate.parseBuilder PlainDate.ofYearMonthDay? input
-
-/--
-Converts a date in the Lean format (`uuuu-MM-dd`) into a `String`.
--/
-def toLeanDateString (input : PlainDate) : String :=
-  Formats.leanDate.formatBuilder input.year input.month input.day
-
 /--
 Parses a `String` in the `AmericanDate` or `SQLDate` format and returns a `PlainDate`.
 -/
 def parse (input : String) : Except String PlainDate :=
-  fromAmericanDateString input
-  <|> fromSQLDateString input
+  Formats.americanDate.parseBuilder (fun m d y => PlainDate.ofYearMonthDay? y m d) input
+  <|> Formats.sqlDate.parseBuilder PlainDate.ofYearMonthDay? input
+
+def leanDateString (d : PlainDate) : String :=
+  Formats.leanDate.formatBuilder d.year d.month d.day
 
 instance : ToString PlainDate where
-  toString := toLeanDateString
+  toString := leanDateString
 
 instance : Repr PlainDate where
-  reprPrec data := Repr.addAppParen ("date(\"" ++ toLeanDateString data ++ "\")")
+  reprPrec d := Repr.addAppParen ("date(\"" ++ leanDateString d ++ "\")")
 
 end PlainDate
 
@@ -260,7 +291,7 @@ namespace PlainTime
 Formats a `PlainTime` using a specific format.
 -/
 def format (time : PlainTime) (format : String) : String :=
-  let format : Except String (GenericFormat .any) := GenericFormat.spec format
+  let format : Except String (Format Awareness.any) := Format.spec format
   match format with
   | .error err => s!"error: {err}"
   | .ok res =>
@@ -271,6 +302,16 @@ def format (time : PlainTime) (format : String) : String :=
       | .n _ => some time.nanosecond
       | .s _ => some time.second
       | .a _ => some (HourMarker.ofOrdinal time.hour)
+      | .b _ =>
+        let h := time.hour.val
+        let m := time.minute.val
+        let s := time.second.val
+        let n := time.nanosecond.val
+        some <|
+          if h = 12 ∧ m = 0 ∧ s = 0 ∧ n = 0 then .noon
+          else if h = 0 ∧ m = 0 ∧ s = 0 ∧ n = 0 then .midnight
+          else if h < 12 then .am
+          else .pm
       | .h _ => some time.hour.toRelative
       | .K _ => some (time.hour.emod 12 (by decide))
       | .S _ => some time.nanosecond
@@ -282,58 +323,24 @@ def format (time : PlainTime) (format : String) : String :=
     | none => "invalid time"
 
 /--
-Parses a time string in the 24-hour format (`HH:mm:ss`) and returns a `PlainTime`.
--/
-def fromTime24Hour (input : String) : Except String PlainTime :=
-  Formats.time24Hour.parseBuilder (fun h m s => some (PlainTime.ofHourMinuteSeconds h m s)) input
-
-/--
-Formats a `PlainTime` value into a 24-hour format string (`HH:mm:ss`).
--/
-def toTime24Hour (input : PlainTime) : String :=
-  Formats.time24Hour.formatBuilder input.hour input.minute input.second
-
-/--
-Parses a time string in the lean 24-hour format (`HH:mm:ss.SSSSSSSSS` or `HH:mm:ss`) and returns a `PlainTime`.
--/
-def fromLeanTime24Hour (input : String) : Except String PlainTime :=
-  Formats.leanTime24Hour.parseBuilder (fun h m s n => some <| PlainTime.ofHourMinuteSecondsNano h m s n) input
-  <|> Formats.leanTime24HourNoNanos.parseBuilder (fun h m s => some <| PlainTime.ofHourMinuteSecondsNano h m s 0) input
-
-/--
-Formats a `PlainTime` value into a 24-hour format string (`HH:mm:ss.SSSSSSSSS`).
--/
-def toLeanTime24Hour (input : PlainTime) : String :=
-  Formats.leanTime24Hour.formatBuilder input.hour input.minute input.second input.nanosecond
-
-/--
-Parses a time string in the 12-hour format (`hh:mm:ss aa`) and returns a `PlainTime`.
--/
-def fromTime12Hour (input : String) : Except String PlainTime := do
-  let builder h m s a : Option PlainTime := do
-    let value ← Internal.Bounded.ofInt? h.val
-    some <| PlainTime.ofHourMinuteSeconds (HourMarker.toAbsolute a value) m s
-
-  Formats.time12Hour.parseBuilder builder input
-
-/--
-Formats a `PlainTime` value into a 12-hour format string (`hh:mm:ss aa`).
--/
-def toTime12Hour (input : PlainTime) : String :=
-  Formats.time12Hour.formatBuilder (input.hour.emod 12 (by decide) |>.add 1) input.minute input.second (if input.hour.val ≥ 12 then HourMarker.pm else HourMarker.am)
-
-/--
-Parses a `String` in the `Time12Hour` or `Time24Hour` format and returns a `PlainTime`.
+Parses a `String` in the `Time12Hour`, `Time24Hour`, or lean time (with optional nanoseconds) format
+and returns a `PlainTime`.
 -/
 def parse (input : String) : Except String PlainTime :=
-  fromTime12Hour input
-  <|> fromTime24Hour input
+  Formats.time12Hour.parseBuilder (fun h m s a => do
+    let value ← Internal.Bounded.ofInt? h.val
+    some <| PlainTime.ofHourMinuteSeconds (HourMarker.toAbsolute a value) m s) input
+  <|> Formats.leanTime24Hour.parseBuilder (fun h m s n => some <| PlainTime.ofHourMinuteSecondsNano h m s n) input
+  <|> Formats.time24Hour.parseBuilder (fun h m s => some (PlainTime.ofHourMinuteSeconds h m s)) input
+
+def leanTimeString (t : PlainTime) : String :=
+  Formats.leanTime24Hour.formatBuilder t.hour t.minute t.second t.nanosecond
 
 instance : ToString PlainTime where
-  toString := toLeanTime24Hour
+  toString := leanTimeString
 
 instance : Repr PlainTime where
-  reprPrec data := Repr.addAppParen ("time(\"" ++ toLeanTime24Hour data ++ "\")")
+  reprPrec data := Repr.addAppParen ("time(\"" ++ leanTimeString data ++ "\")")
 
 end PlainTime
 
@@ -343,99 +350,60 @@ namespace ZonedDateTime
 Formats a `ZonedDateTime` using a specific format.
 -/
 def format (data: ZonedDateTime) (format : String) : String :=
-  let format : Except String (GenericFormat .any) := GenericFormat.spec format
+  let format : Except String (Format Awareness.any) := Format.spec format
   match format with
   | .error err => s!"error: {err}"
-  | .ok res => res.format data.toDateTime
+  | .ok res => res.format data
 
 /--
-Parses a `String` in the `ISO8601` format and returns a `ZonedDateTime`.
+Parses a `String` in common zoned date-time formats and returns a `ZonedDateTime`.
+This parser does not resolve timezone identifiers like `[Europe/Paris]`; use `parseIO` for that.
 -/
-def fromISO8601String (input : String) : Except String ZonedDateTime :=
-  Formats.iso8601.parse input
+-- Wraps Format.parse to fix type unification (Awareness.any.type vs ZonedDateTime).
+private def parseFormat (fmt : Format Awareness.any) (input : String) : Except String ZonedDateTime :=
+  fmt.parse input
 
-/--
-Formats a `ZonedDateTime` value into an ISO8601 string.
--/
-def toISO8601String (date : ZonedDateTime) : String :=
-  Formats.iso8601.format date.toDateTime
-
-/--
-Parses a `String` in the rfc822 format and returns a `ZonedDateTime`.
--/
-def fromRFC822String (input : String) : Except String ZonedDateTime :=
-  Formats.rfc822.parse input
-
-/--
-Formats a `ZonedDateTime` value into an RFC822 format string.
--/
-def toRFC822String (date : ZonedDateTime) : String :=
-  Formats.rfc822.format date.toDateTime
-
-/--
-Parses a `String` in the rfc850 format and returns a `ZonedDateTime`.
--/
-def fromRFC850String (input : String) : Except String ZonedDateTime :=
-  Formats.rfc850.parse input
-
-/--
-Formats a `ZonedDateTime` value into an RFC850 format string.
--/
-def toRFC850String (date : ZonedDateTime) : String :=
-  Formats.rfc850.format date.toDateTime
-
-/--
-Parses a `String` in the dateTimeWithZone format and returns a `ZonedDateTime` object in the GMT time zone.
--/
-def fromDateTimeWithZoneString (input : String) : Except String ZonedDateTime :=
-  Formats.dateTimeWithZone.parse input
-
-/--
-Formats a `ZonedDateTime` value into a simple date time with timezone string.
--/
-def toDateTimeWithZoneString (pdt : ZonedDateTime) : String :=
-  Formats.dateTimeWithZone.format pdt.toDateTime
-
-/--
-Parses a `String` in the lean date time format with timezone format and returns a `ZonedDateTime` object.
--/
-def fromLeanDateTimeWithZoneString (input : String) : Except String ZonedDateTime :=
-  Formats.leanDateTimeWithZone.parse input
-  <|> Formats.leanDateTimeWithZoneNoNanos.parse input
-
-/--
-Parses a `String` in the lean date time format with identifier and returns a `ZonedDateTime` object.
--/
-def fromLeanDateTimeWithIdentifierString (input : String) : Except String ZonedDateTime :=
-  Formats.leanDateTimeWithIdentifier.parse input
-  <|> Formats.leanDateTimeWithIdentifierAndNanos.parse input
-
-/--
-Formats a `DateTime` value into a simple date time with timezone string that can be parsed by the date% notation.
--/
-def toLeanDateTimeWithZoneString (zdt : ZonedDateTime) : String :=
-  Formats.leanDateTimeWithZone.formatBuilder zdt.year zdt.month zdt.day zdt.hour zdt.minute zdt.date.get.time.second zdt.nanosecond zdt.offset
-/--
-Formats a `DateTime` value into a simple date time with timezone string that can be parsed by the date% notation with the timezone identifier.
--/
-def toLeanDateTimeWithIdentifierString (zdt : ZonedDateTime) : String :=
-  Formats.leanDateTimeWithIdentifierAndNanos.formatBuilder zdt.year zdt.month zdt.day zdt.hour zdt.minute zdt.date.get.time.second zdt.nanosecond zdt.timezone.name
-
-/--
-Parses a `String` in the `ISO8601`, `RFC822` or `RFC850` format and returns a `ZonedDateTime`.
--/
 def parse (input : String) : Except String ZonedDateTime :=
-  fromISO8601String input
-  <|> fromRFC822String input
-  <|> fromRFC850String input
-  <|> fromDateTimeWithZoneString input
-  <|> fromLeanDateTimeWithIdentifierString input
+  parseFormat Formats.iso8601 input
+  <|> parseFormat Formats.rfc822 input
+  <|> parseFormat Formats.rfc850 input
+  <|> parseFormat Formats.leanDateTimeWithZone input
+  <|> parseFormat Formats.leanDateTimeWithZoneNoNanos input
+  <|> parseFormat Formats.leanDateTimeWithZoneAndName input
+  <|> parseFormat Formats.leanDateTimeWithZoneAndNameNoNanos input
+  <|> parseFormat Formats.dateTimeWithZone input
+  <|> parseFormat Formats.leanDateTimeWithIdentifier input
+  <|> parseFormat Formats.leanDateTimeWithIdentifierAndNanos input
+
+/--
+Parses a `String` in common zoned date-time formats.
+If the input uses a timezone identifier (for example, `[Europe/Paris]`), it resolves it using the default timezone database.
+-/
+def parseIO (input : String) : IO ZonedDateTime := do
+  match parse input with
+  | .ok zdt => pure zdt
+  | .error err =>
+    let identParse : Except String ZonedDateTime :=
+      Formats.leanDateTimeWithIdentifier.parseUnchecked input
+      <|> Formats.leanDateTimeWithIdentifierAndNanos.parseUnchecked input
+    match identParse with
+    | .ok zdt =>
+      let rules ← Database.defaultGetZoneRules zdt.timezone.name
+      pure <| ZonedDateTime.ofPlainDateTime zdt.toPlainDateTime rules
+    | .error _ => throw <| IO.userError err
 
 instance : ToString ZonedDateTime where
-  toString := toLeanDateTimeWithIdentifierString
+  toString data := Formats.leanDateTimeWithIdentifierAndNanos.format data
 
 instance : Repr ZonedDateTime where
-  reprPrec data := Repr.addAppParen ("zoned(\"" ++ toLeanDateTimeWithZoneString data ++ "\")")
+  reprPrec data :=
+    let name := data.timezone.name
+    let str :=
+      if name == data.timezone.offset.toIsoString true then
+        Formats.leanDateTimeWithZone.format data
+      else
+        Formats.leanDateTimeWithZoneAndName.format data
+    Repr.addAppParen ("zoned(\"" ++ str ++ "\")")
 
 end ZonedDateTime
 
@@ -445,22 +413,31 @@ namespace PlainDateTime
 Formats a `PlainDateTime` using a specific format.
 -/
 def format (date : PlainDateTime) (format : String) : String :=
-  let format : Except String (GenericFormat .any) := GenericFormat.spec format
+  let format : Except String (Format Awareness.any) := Format.spec format
   match format with
   | .error err => s!"error: {err}"
   | .ok res =>
     let res := res.formatGeneric fun
       | .G _ => some date.era
       | .y _ => some date.year
+      | .Y _ =>
+        let week := date.weekOfYear
+        some <|
+          if date.month.val = 1 ∧ week.val ≥ 52 then
+            date.year - 1
+          else if date.month.val = 12 ∧ week.val = 1 then
+            date.year + 1
+          else
+            date.year
       | .u _ => some date.year
       | .D _ => some (Sigma.mk date.year.isLeap date.dayOfYear)
-      | .Qorq _ => some date.quarter
+      | .Q _ | .q _ => some date.quarter
       | .w _ => some date.weekOfYear
-      | .W _ => some date.alignedWeekOfMonth
-      | .MorL _ => some date.month
+      | .W _ => some date.weekOfMonth
+      | .M _ | .L _ => some date.month
       | .d _ => some date.day
       | .E _ => some date.weekday
-      | .eorc _ => some date.weekday
+      | .e _ | .c _ => some date.weekday
       | .F _ => some date.weekOfMonth
       | .H _ => some date.hour
       | .k _ => some date.hour.shiftTo1BasedHour
@@ -479,71 +456,22 @@ def format (date : PlainDateTime) (format : String) : String :=
     | none => "invalid time"
 
 /--
-Parses a `String` in the `AscTime` format and returns a `PlainDateTime` object in the GMT time zone.
--/
-def fromAscTimeString (input : String) : Except String PlainDateTime :=
-  Formats.ascTime.parse input
-  |>.map DateTime.toPlainDateTime
-
-/--
-Formats a `PlainDateTime` value into an AscTime format string.
--/
-def toAscTimeString (pdt : PlainDateTime) : String :=
-  Formats.ascTime.format (DateTime.ofPlainDateTimeAssumingUTC pdt .UTC)
-
-/--
-Parses a `String` in the `LongDateFormat` and returns a `PlainDateTime` object in the GMT time zone.
--/
-def fromLongDateFormatString (input : String) : Except String PlainDateTime :=
-  Formats.longDateFormat.parse input
-  |>.map DateTime.toPlainDateTime
-
-/--
-Formats a `PlainDateTime` value into a LongDateFormat string.
--/
-def toLongDateFormatString (pdt : PlainDateTime) : String :=
-  Formats.longDateFormat.format (DateTime.ofPlainDateTimeAssumingUTC pdt .UTC)
-
-/--
-Parses a `String` in the `DateTime` format and returns a `PlainDateTime`.
--/
-def fromDateTimeString (input : String) : Except String PlainDateTime :=
-  Formats.dateTime24Hour.parse input
-  |>.map DateTime.toPlainDateTime
-
-/--
-Formats a `PlainDateTime` value into a `DateTime` format string.
--/
-def toDateTimeString (pdt : PlainDateTime) : String :=
-  Formats.dateTime24Hour.formatBuilder pdt.year pdt.month pdt.day pdt.hour pdt.minute pdt.time.second pdt.nanosecond
-
-/--
-Parses a `String` in the `DateTime` format and returns a `PlainDateTime`.
--/
-def fromLeanDateTimeString (input : String) : Except String PlainDateTime :=
-  (Formats.leanDateTime24Hour.parse input <|> Formats.leanDateTime24HourNoNanos.parse input)
-  |>.map DateTime.toPlainDateTime
-
-/--
-Formats a `PlainDateTime` value into a `DateTime` format string.
--/
-def toLeanDateTimeString (pdt : PlainDateTime) : String :=
-  Formats.leanDateTime24Hour.formatBuilder pdt.year pdt.month pdt.day pdt.hour pdt.minute pdt.time.second pdt.nanosecond
-
-/--
-Parses a `String` in the `AscTime` or `LongDate` format and returns a `PlainDateTime`.
+Parses a `String` in the `AscTime`, `LongDate`, `DateTime`, or `LeanDateTime` format and returns a `PlainDateTime`.
 -/
 def parse (date : String) : Except String PlainDateTime :=
-  fromAscTimeString date
-  <|> fromLongDateFormatString date
-  <|> fromDateTimeString date
-  <|> fromLeanDateTimeString date
+  (Formats.ascTime.parse date).map DateTime.toPlainDateTime
+  <|> (Formats.longDateFormat.parse date).map DateTime.toPlainDateTime
+  <|> (Formats.dateTime24Hour.parse date).map DateTime.toPlainDateTime
+  <|> (Formats.leanDateTime24HourAlt.parse date).map DateTime.toPlainDateTime
+
+def leanPlainDateTimeString (date : PlainDateTime) : String :=
+  Formats.leanDateTime24Hour.formatBuilder date.year date.month date.day date.hour date.minute date.time.second date.nanosecond
 
 instance : ToString PlainDateTime where
-  toString := toLeanDateTimeString
+  toString := leanPlainDateTimeString
 
 instance : Repr PlainDateTime where
-  reprPrec data := Repr.addAppParen ("datetime(\"" ++ toLeanDateTimeString data ++ "\")")
+  reprPrec data := Repr.addAppParen ("datetime(\"" ++ leanPlainDateTimeString data ++ "\")")
 
 end PlainDateTime
 
@@ -553,76 +481,22 @@ namespace DateTime
 Formats a `DateTime` using a specific format.
 -/
 def format (data: DateTime tz) (format : String) : String :=
-  let format : Except String (GenericFormat .any) := GenericFormat.spec format
+  let format : Except String (Format Awareness.any) := Format.spec format
   match format with
   | .error err => s!"error: {err}"
   | .ok res => res.format data
 
-/--
-Parses a `String` in the `AscTime` format and returns a `DateTime` object in the GMT time zone.
--/
-def fromAscTimeString (input : String) : Except String (DateTime .GMT) :=
-  Formats.ascTime.parse input
-
-/--
-Formats a `DateTime` value into an AscTime format string.
--/
-def toAscTimeString (datetime : DateTime .GMT) : String :=
-  Formats.ascTime.format datetime
-
-/--
-Parses a `String` in the `LongDateFormat` and returns a `DateTime` object in the GMT time zone.
--/
-def fromLongDateFormatString (input : String) : Except String (DateTime .GMT) :=
-  Formats.longDateFormat.parse input
-
-/--
-Formats a `DateTime` value into a LongDateFormat string.
--/
-def toLongDateFormatString (datetime : DateTime .GMT) : String :=
-  Formats.longDateFormat.format datetime
-
-/--
-Formats a `DateTime` value into an ISO8601 string.
--/
-def toISO8601String (date : DateTime tz) : String :=
-  Formats.iso8601.format date
-
-/--
-Formats a `DateTime` value into an RFC822 format string.
--/
-def toRFC822String (date : DateTime tz) : String :=
-  Formats.rfc822.format date
-
-/--
-Formats a `DateTime` value into an RFC850 format string.
--/
-def toRFC850String (date : DateTime tz) : String :=
-  Formats.rfc850.format date
-
-/--
-Formats a `DateTime` value into a `DateTimeWithZone` format string.
--/
-def toDateTimeWithZoneString (pdt : DateTime tz) : String :=
-  Formats.dateTimeWithZone.format pdt
-
-/--
-Formats a `DateTime` value into a `DateTimeWithZone` format string that can be parsed by `date%`.
--/
-def toLeanDateTimeWithZoneString (pdt : DateTime tz) : String :=
-  Formats.leanDateTimeWithZone.format pdt
-
 /--
 Parses a `String` in the `AscTime` or `LongDate` format and returns a `DateTime`.
 -/
 def parse (date : String) : Except String (DateTime .GMT) :=
-  fromAscTimeString date
-  <|> fromLongDateFormatString date
+  Formats.ascTime.parse date
+  <|> Formats.longDateFormat.parse date
 
 instance : Repr (DateTime tz) where
-  reprPrec data := Repr.addAppParen (toLeanDateTimeWithZoneString data)
+  reprPrec data := Repr.addAppParen (Formats.leanDateTimeWithZone.format data)
 
 instance : ToString (DateTime tz) where
-  toString := toLeanDateTimeWithZoneString
+  toString data := Formats.leanDateTimeWithZone.format data
 
 end DateTime

src/Std/Time/Notation.lean

@@ -21,6 +21,7 @@ private meta def convertText : Text → MacroM (TSyntax `term)
   | .short  => `(Std.Time.Text.short)
   | .full   => `(Std.Time.Text.full)
   | .narrow => `(Std.Time.Text.narrow)
+  | .twoLetterShort => `(Std.Time.Text.twoLetterShort)
 
 private meta def convertNumber : Number → MacroM (TSyntax `term)
   | ⟨padding⟩ => `(Std.Time.Number.mk $(quote padding))
@@ -58,26 +59,40 @@ private meta def convertOffsetZ : OffsetZ → MacroM (TSyntax `term)
 private meta def convertModifier : Modifier → MacroM (TSyntax `term)
   | .G p => do `(Std.Time.Modifier.G $(← convertText p))
   | .y p => do `(Std.Time.Modifier.y $(← convertYear p))
+  | .Y p => do `(Std.Time.Modifier.Y $(← convertYear p))
   | .u p => do `(Std.Time.Modifier.u $(← convertYear p))
   | .D p => do `(Std.Time.Modifier.D $(← convertNumber p))
-  | .MorL p =>
+  | .M p =>
     match p with
-    | .inl num => do `(Std.Time.Modifier.MorL (.inl $(← convertNumber num)))
-    | .inr txt => do `(Std.Time.Modifier.MorL (.inr $(← convertText txt)))
+    | .inl num => do `(Std.Time.Modifier.M (.inl $(← convertNumber num)))
+    | .inr txt => do `(Std.Time.Modifier.M (.inr $(← convertText txt)))
+  | .L p =>
+    match p with
+    | .inl num => do `(Std.Time.Modifier.L (.inl $(← convertNumber num)))
+    | .inr txt => do `(Std.Time.Modifier.L (.inr $(← convertText txt)))
   | .d p => do `(Std.Time.Modifier.d $(← convertNumber p))
-  | .Qorq p =>
+  | .Q p =>
     match p with
-    | .inl num => do `(Std.Time.Modifier.Qorq (.inl $(← convertNumber num)))
-    | .inr txt => do `(Std.Time.Modifier.Qorq (.inr $(← convertText txt)))
+    | .inl num => do `(Std.Time.Modifier.Q (.inl $(← convertNumber num)))
+    | .inr txt => do `(Std.Time.Modifier.Q (.inr $(← convertText txt)))
+  | .q p =>
+    match p with
+    | .inl num => do `(Std.Time.Modifier.q (.inl $(← convertNumber num)))
+    | .inr txt => do `(Std.Time.Modifier.q (.inr $(← convertText txt)))
   | .w p => do `(Std.Time.Modifier.w $(← convertNumber p))
   | .W p => do `(Std.Time.Modifier.W $(← convertNumber p))
   | .E p => do `(Std.Time.Modifier.E $(← convertText p))
-  | .eorc p =>
+  | .e p =>
     match p with
-    | .inl num => do `(Std.Time.Modifier.eorc (.inl $(← convertNumber num)))
-    | .inr txt => do `(Std.Time.Modifier.eorc (.inr $(← convertText txt)))
+    | .inl num => do `(Std.Time.Modifier.e (.inl $(← convertNumber num)))
+    | .inr txt => do `(Std.Time.Modifier.e (.inr $(← convertText txt)))
+  | .c p =>
+    match p with
+    | .inl num => do `(Std.Time.Modifier.c (.inl $(← convertNumber num)))
+    | .inr txt => do `(Std.Time.Modifier.c (.inr $(← convertText txt)))
   | .F p => do `(Std.Time.Modifier.F $(← convertNumber p))
   | .a p => do `(Std.Time.Modifier.a $(← convertText p))
+  | .b p => do `(Std.Time.Modifier.b $(← convertText p))
   | .h p => do `(Std.Time.Modifier.h $(← convertNumber p))
   | .K p => do `(Std.Time.Modifier.K $(← convertNumber p))
   | .k p => do `(Std.Time.Modifier.k $(← convertNumber p))
@@ -88,8 +103,9 @@ private meta def convertModifier : Modifier → MacroM (TSyntax `term)
   | .A p => do `(Std.Time.Modifier.A $(← convertNumber p))
   | .n p => do `(Std.Time.Modifier.n $(← convertNumber p))
   | .N p => do `(Std.Time.Modifier.N $(← convertNumber p))
-  | .V => `(Std.Time.Modifier.V)
+  | .V p => do `(Std.Time.Modifier.V $(← convertNumber p))
   | .z p => do `(Std.Time.Modifier.z $(← convertZoneName p))
+  | .v p => do `(Std.Time.Modifier.v $(← convertZoneName p))
   | .O p => do `(Std.Time.Modifier.O $(← convertOffsetO p))
   | .X p => do `(Std.Time.Modifier.X $(← convertOffsetX p))
   | .x p => do `(Std.Time.Modifier.x $(← convertOffsetX p))
@@ -207,33 +223,40 @@ syntax "timezone(" str ")" : term
 
 macro_rules
   | `(zoned( $date:str )) => do
-      match ZonedDateTime.fromLeanDateTimeWithZoneString date.getString with
+      let s := date.getString
+      match (Formats.leanDateTimeWithZoneAlt.parse s : Except String ZonedDateTime) with
       | .ok res => do return ← convertZonedDateTime res
       | .error _ =>
-        match ZonedDateTime.fromLeanDateTimeWithIdentifierString date.getString with
-        | .ok res => do return ← convertZonedDateTime res (identifier := true)
-        | .error res => Macro.throwErrorAt date s!"error: {res}"
+        match (Formats.leanDateTimeWithZoneAndNameAlt.parse s : Except String ZonedDateTime) with
+        | .ok res => do return ← convertZonedDateTime res
+        | .error _ =>
+          let identParse : Except String ZonedDateTime :=
+            Formats.leanDateTimeWithIdentifier.parseUnchecked s
+            <|> Formats.leanDateTimeWithIdentifierAndNanos.parseUnchecked s
+          match identParse with
+          | .ok res => do return ← convertZonedDateTime res (identifier := true)
+          | .error res => Macro.throwErrorAt date s!"error: {res}"
 
   | `(zoned( $date:str, $timezone )) => do
-      match PlainDateTime.fromLeanDateTimeString date.getString with
+      match (Formats.leanDateTime24HourAlt.parse date.getString).map DateTime.toPlainDateTime with
       | .ok res => do
         let plain ← convertPlainDateTime res
         `(Std.Time.ZonedDateTime.ofPlainDateTime $plain $timezone)
       | .error res => Macro.throwErrorAt date s!"error: {res}"
 
   | `(datetime( $date:str )) => do
-      match PlainDateTime.fromLeanDateTimeString date.getString with
+      match (Formats.leanDateTime24HourAlt.parse date.getString).map DateTime.toPlainDateTime with
       | .ok res => do
         return ← convertPlainDateTime res
       | .error res => Macro.throwErrorAt date s!"error: {res}"
 
   | `(date( $date:str )) => do
-      match PlainDate.fromSQLDateString date.getString with
+      match PlainDate.parse date.getString with
       | .ok res => return ← convertPlainDate res
       | .error res => Macro.throwErrorAt date s!"error: {res}"
 
   | `(time( $time:str )) => do
-      match PlainTime.fromLeanTime24Hour time.getString with
+      match PlainTime.parse time.getString with
       | .ok res => return ← convertPlainTime res
       | .error res => Macro.throwErrorAt time s!"error: {res}"
 

src/Std/Time/Notation/Spec.lean

@@ -19,6 +19,7 @@ private meta def convertText : Text → MacroM (TSyntax `term)
   | .short => `(Std.Time.Text.short)
   | .full => `(Std.Time.Text.full)
   | .narrow => `(Std.Time.Text.narrow)
+  | .twoLetterShort => `(Std.Time.Text.twoLetterShort)
 
 private meta def convertNumber : Number → MacroM (TSyntax `term)
   | ⟨padding⟩ => `(Std.Time.Number.mk $(quote padding))
@@ -56,26 +57,40 @@ private meta def convertOffsetZ : OffsetZ → MacroM (TSyntax `term)
 private meta def convertModifier : Modifier → MacroM (TSyntax `term)
   | .G p => do `(Std.Time.Modifier.G $(← convertText p))
   | .y p => do `(Std.Time.Modifier.y $(← convertYear p))
+  | .Y p => do `(Std.Time.Modifier.Y $(← convertYear p))
   | .u p => do `(Std.Time.Modifier.u $(← convertYear p))
   | .D p => do `(Std.Time.Modifier.D $(← convertNumber p))
-  | .MorL p =>
+  | .M p =>
     match p with
-    | .inl num => do `(Std.Time.Modifier.MorL (.inl $(← convertNumber num)))
-    | .inr txt => do `(Std.Time.Modifier.MorL (.inr $(← convertText txt)))
+    | .inl num => do `(Std.Time.Modifier.M (.inl $(← convertNumber num)))
+    | .inr txt => do `(Std.Time.Modifier.M (.inr $(← convertText txt)))
+  | .L p =>
+    match p with
+    | .inl num => do `(Std.Time.Modifier.L (.inl $(← convertNumber num)))
+    | .inr txt => do `(Std.Time.Modifier.L (.inr $(← convertText txt)))
   | .d p => do `(Std.Time.Modifier.d $(← convertNumber p))
-  | .Qorq p =>
+  | .Q p =>
     match p with
-    | .inl num => do `(Std.Time.Modifier.Qorq (.inl $(← convertNumber num)))
-    | .inr txt => do `(Std.Time.Modifier.Qorq (.inr $(← convertText txt)))
+    | .inl num => do `(Std.Time.Modifier.Q (.inl $(← convertNumber num)))
+    | .inr txt => do `(Std.Time.Modifier.Q (.inr $(← convertText txt)))
+  | .q p =>
+    match p with
+    | .inl num => do `(Std.Time.Modifier.q (.inl $(← convertNumber num)))
+    | .inr txt => do `(Std.Time.Modifier.q (.inr $(← convertText txt)))
   | .w p => do `(Std.Time.Modifier.w $(← convertNumber p))
   | .W p => do `(Std.Time.Modifier.W $(← convertNumber p))
   | .E p => do `(Std.Time.Modifier.E $(← convertText p))
-  | .eorc p =>
+  | .e p =>
     match p with
-    | .inl num => do `(Std.Time.Modifier.eorc (.inl $(← convertNumber num)))
-    | .inr txt => do `(Std.Time.Modifier.eorc (.inr $(← convertText txt)))
+    | .inl num => do `(Std.Time.Modifier.e (.inl $(← convertNumber num)))
+    | .inr txt => do `(Std.Time.Modifier.e (.inr $(← convertText txt)))
+  | .c p =>
+    match p with
+    | .inl num => do `(Std.Time.Modifier.c (.inl $(← convertNumber num)))
+    | .inr txt => do `(Std.Time.Modifier.c (.inr $(← convertText txt)))
   | .F p => do `(Std.Time.Modifier.F $(← convertNumber p))
   | .a p => do `(Std.Time.Modifier.a $(← convertText p))
+  | .b p => do `(Std.Time.Modifier.b $(← convertText p))
   | .h p => do `(Std.Time.Modifier.h $(← convertNumber p))
   | .K p => do `(Std.Time.Modifier.K $(← convertNumber p))
   | .k p => do `(Std.Time.Modifier.k $(← convertNumber p))
@@ -86,8 +101,9 @@ private meta def convertModifier : Modifier → MacroM (TSyntax `term)
   | .A p => do `(Std.Time.Modifier.A $(← convertNumber p))
   | .n p => do `(Std.Time.Modifier.n $(← convertNumber p))
   | .N p => do `(Std.Time.Modifier.N $(← convertNumber p))
-  | .V => `(Std.Time.Modifier.V)
+  | .V p => do `(Std.Time.Modifier.V $(← convertNumber p))
   | .z p => do `(Std.Time.Modifier.z $(← convertZoneName p))
+  | .v p => do `(Std.Time.Modifier.v $(← convertZoneName p))
   | .O p => do `(Std.Time.Modifier.O $(← convertOffsetO p))
   | .X p => do `(Std.Time.Modifier.X $(← convertOffsetX p))
   | .x p => do `(Std.Time.Modifier.x $(← convertOffsetX p))
@@ -109,7 +125,7 @@ syntax "datespec(" str "," term ")" : term
 
 private meta def formatStringToFormat (fmt : TSyntax `str) (config : Option (TSyntax `term)) : MacroM (TSyntax `term) := do
   let input := fmt.getString
-  let format : Except String (GenericFormat .any) := GenericFormat.spec input
+  let format : Except String (Format .any) := Format.spec input
   match format with
   | .ok res =>
     let alts ← res.string.mapM convertFormatPart

src/Std/Time/Zoned/DateTime.lean

@@ -410,9 +410,17 @@ def weekday (dt : DateTime tz) : Weekday :=
 /--
 Determines the era of the given `DateTime` based on its year.
 -/
+@[inline]
 def era (date : DateTime tz) : Year.Era :=
   date.year.era
 
+/--
+Returns the week-based year for a given `DateTime`.
+-/
+@[inline]
+def weekBasedYear (date : DateTime tz) : Year.Offset :=
+  date.date.get.weekBasedYear
+
 /--
 Sets the `DateTime` to the specified `desiredWeekday`.
 -/

src/Std/Time/Zoned/ZonedDateTime.lean

@@ -15,8 +15,7 @@ public section
 namespace Std
 namespace Time
 
--- TODO (@kim-em): re-enable this once there is a mechanism to exclude `linter.indexVariables`.
--- set_option linter.all true
+set_option linter.all true
 
 /--
 Represents a date and time with timezone information.
@@ -153,6 +152,13 @@ Getter for the `Year` inside of a `ZonedDateTime`
 def year (zdt : ZonedDateTime) : Year.Offset :=
   zdt.date.get.year
 
+/--
+Returns the week-based year for a given `ZonedDateTime`.
+-/
+@[inline]
+def weekBasedYear (zdt : ZonedDateTime) : Year.Offset :=
+  zdt.date.get.weekBasedYear
+
 /--
 Getter for the `Month` inside of a `ZonedDateTime`
 -/

tests/elab/dateTimeOrd.lean

@@ -45,4 +45,4 @@ example : Std.LawfulBEqOrd (DateTime TimeZone.GMT) := inferInstance
    "Sat Jan 01 02:01:01 2025",
    "Sat Jan 02 01:01:01 2025",
    "Sat Feb 01 01:01:01 2025",
-   "Sat Jan 01 01:01:01 2026"].map (DateTime.fromAscTimeString . |>.toOption.get!)
+   "Sat Jan 01 01:01:01 2026"].map (DateTime.parse · |>.toOption.get!)

tests/elab/grind_mon_order.lean

@@ -1,6 +1,6 @@
 module
 public import Init.Grind.Ring.CommSolver
-public import Lean.Meta.Sym.Arith.Poly
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 open Lean.Grind.CommRing
 
 def w : Var := 0

tests/elab/grind_spoly.lean

@@ -1,5 +1,5 @@
 module
-import Lean.Meta.Sym.Arith.Poly
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 open Lean.Grind.CommRing
 
 def w : Expr := .var 0

tests/elab/sym_arith_classify.lean

@@ -1,138 +0,0 @@
-import Lean
-
-/-!
-# Tests for `Sym.Arith.Classify`, `Sym.Arith.EvalNum`, and `Sym.Arith.Functions`
--/
-
-open Lean Meta Sym Arith
-
-/-- Extract the value of a definition by name. -/
-def getDefValue (n : Name) : MetaM Expr := do
-  let some (.defnInfo info) := (← getEnv).find? n
-    | throwError "expected definition: {n}"
-  return info.value
-
-/-! ## Classification tests -/
-
-deriving instance Repr for ClassifyResult
-
-/-- info: Lean.Meta.Sym.Arith.ClassifyResult.commRing 0 -/
-#guard_msgs in
-run_meta SymM.run do
-  logInfo m!"{repr (← classify? (mkConst ``Int))}"
-
-/-- info: Lean.Meta.Sym.Arith.ClassifyResult.commSemiring 0 -/
-#guard_msgs in
-run_meta SymM.run do
-  logInfo m!"{repr (← classify? (mkConst ``Nat))}"
-
-/-- info: Lean.Meta.Sym.Arith.ClassifyResult.none -/
-#guard_msgs in
-run_meta SymM.run do
-  logInfo m!"{repr (← classify? (mkConst ``Bool))}"
-
--- Classifying the same type twice should return cached result with same id
-/-- info: true -/
-#guard_msgs in
-run_meta SymM.run do
-  let .commRing id1 ← classify? (mkConst ``Int) | unreachable!
-  let .commRing id2 ← classify? (mkConst ``Int) | unreachable!
-  logInfo m!"{id1 == id2}"
-
-/--
-info: Lean.Meta.Sym.Arith.ClassifyResult.commRing 0
----
-info: Lean.Meta.Sym.Arith.ClassifyResult.commSemiring 0
----
-info: Lean.Meta.Sym.Arith.ClassifyResult.commRing 2
----
-info: Lean.Meta.Sym.Arith.ClassifyResult.commRing 1
--/
-#guard_msgs in
-run_meta SymM.run do
-  let int ← shareCommon (mkConst ``Int)
-  let nat ← shareCommon (mkConst ``Nat)
-  let rat ← shareCommon (mkConst ``Rat)
-  logInfo m!"{repr (← classify? int)}"
-  logInfo m!"{repr (← classify? nat)}"
-  logInfo m!"{repr (← classify? rat)}"
-  let inst ← Sym.synthInstance (mkApp (mkConst ``Grind.Semiring [0]) nat)
-  let ofSemiring ← shareCommon (← Sym.canon <| mkApp2 (mkConst ``Grind.Ring.OfSemiring.Q [0]) nat inst)
-  logInfo m!"{repr (← classify? ofSemiring)}"
-
-/-! ## EvalNum tests -/
-
-def natZero : Nat := 0
-def natSucc3 : Nat := Nat.succ (Nat.succ (Nat.succ 0))
-def natSeven : Nat := 7
-def natAdd : Nat := 2 + 3
-def natMul : Nat := 2 * 3
-def natPow : Nat := 2 ^ 3
-def natBigPow : Nat := 2 ^ 100
-def natPow10 : Nat := 2 ^ 10
-
-/-- info: some (0) -/
-#guard_msgs in
-run_meta SymM.run do
-  logInfo m!"{← evalNat? (← getDefValue ``natZero)}"
-
-/-- info: some (3) -/
-#guard_msgs in
-run_meta SymM.run do
-  logInfo m!"{← evalNat? (← getDefValue ``natSucc3)}"
-
-/-- info: some (7) -/
-#guard_msgs in
-run_meta SymM.run do
-  logInfo m!"{← evalNat? (← getDefValue ``natSeven)}"
-
-/-- info: some (5) -/
-#guard_msgs in
-run_meta SymM.run do
-  logInfo m!"{← evalNat? (← getDefValue ``natAdd)}"
-
-/-- info: some (6) -/
-#guard_msgs in
-run_meta SymM.run do
-  logInfo m!"{← evalNat? (← getDefValue ``natMul)}"
-
-/-- info: some (8) -/
-#guard_msgs in
-run_meta SymM.run do
-  logInfo m!"{← evalNat? (← getDefValue ``natPow)}"
-
-/-! ## Exp threshold tests -/
-
--- 2 ^ 100 should fail with default exp threshold (8)
-/-- info: none -/
-#guard_msgs in
-run_meta SymM.run do
-  logInfo m!"{← evalNat? (← getDefValue ``natBigPow)}"
-
--- 2 ^ 10 succeeds with exp threshold raised to 20
-/-- info: some (1024) -/
-#guard_msgs in
-run_meta SymM.run do
-  withExpThreshold 20 do
-    logInfo m!"{← evalNat? (← getDefValue ``natPow10)}"
-
-/-! ## Int EvalNum tests -/
-
-def intNeg : Int := -5
-def intAdd : Int := 3 + (-2)
-def intMul : Int := (-3) * 4
-
-/-- info: some (-5) -/
-#guard_msgs in
-run_meta SymM.run do
-  logInfo m!"{← evalInt? (← getDefValue ``intNeg)}"
-
-/-- info: some (1) -/
-#guard_msgs in
-run_meta SymM.run do
-  logInfo m!"{← evalInt? (← getDefValue ``intAdd)}"
-
-/-- info: some (-12) -/
-#guard_msgs in
-run_meta SymM.run do
-  logInfo m!"{← evalInt? (← getDefValue ``intMul)}"

tests/elab/sym_arith_reify.lean

@@ -1,172 +0,0 @@
-import Lean
-
-/-!
-# Tests for `Sym.Arith.Reify`
--/
-
-open Lean Meta Sym Arith
-
-/-- Extract the value of a definition by name. -/
-def getDefValue (n : Name) : MetaM Expr := do
-  let some (.defnInfo info) := (← getEnv).find? n
-    | throwError "expected definition: {n}"
-  return info.value
-
-/-!
-## Setup: a simple monad for testing reification
--/
-
-structure TestState where
-  ring : CommRing
-  vars : Array Expr := {}
-  varMap : PHashMap ExprPtr Var := {}
-
-abbrev TestM := StateRefT TestState SymM
-
-instance : MonadCanon TestM where
-  canonExpr e := Sym.canon e
-  synthInstance? e := Sym.synthInstance? e
-
-instance : MonadCommRing TestM where
-  getCommRing := return (← get).ring
-  modifyCommRing f := modify fun s => { s with ring := f s.ring }
-
-instance : MonadMkVar TestM where
-  mkVar e := do
-    if let some v := (← get).varMap.find? { expr := e } then
-      return v
-    let v := (← get).vars.size
-    modify fun s => { s with
-      vars := s.vars.push e
-      varMap := s.varMap.insert { expr := e } v
-    }
-    return v
-
-instance : MonadGetVar TestM where
-  getVar x := return (← get).vars[x]!
-
-/-- Run a `TestM` on `Int`'s `CommRing`, canonicalizing `e` first. -/
-def reifyIntExpr (n : Name) (skipVar := true) : TestM (Option RingExpr) := do
-  let e ← canonExpr (← getDefValue n)
-  reifyRing? e (skipVar := skipVar)
-
-def runTestOnInt (x : TestM α) : SymM α := do
-  let .commRing id ← classify? (mkConst ``Int) | throwError "Int is not a CommRing"
-  let ring := (← getArithState).rings[id]!
-  x |>.run' { ring }
-
-/-! ## Reify ring tests on Int -/
-
-deriving instance Repr for Lean.Grind.CommRing.Expr
-
-def intAdd : Int := 2 + 3
-def intMulAdd : Int := 2 * 3 + 1
-def intNeg : Int := -5
-def intPow : Int := 2 ^ 3
-def intSub : Int := 7 - 2
-
-/-- info: some (Lean.Grind.CommRing.Expr.add (Lean.Grind.CommRing.Expr.num 2) (Lean.Grind.CommRing.Expr.num 3)) -/
-#guard_msgs in
-run_meta SymM.run do runTestOnInt do
-  logInfo m!"{repr (← reifyIntExpr ``intAdd)}"
-
-/--
-info: some (Lean.Grind.CommRing.Expr.add
-  (Lean.Grind.CommRing.Expr.mul (Lean.Grind.CommRing.Expr.num 2) (Lean.Grind.CommRing.Expr.num 3))
-  (Lean.Grind.CommRing.Expr.num 1))
--/
-#guard_msgs in
-run_meta SymM.run do runTestOnInt do
-  logInfo m!"{repr (← reifyIntExpr ``intMulAdd)}"
-
-/-- info: some (Lean.Grind.CommRing.Expr.neg (Lean.Grind.CommRing.Expr.num 5)) -/
-#guard_msgs in
-run_meta SymM.run do runTestOnInt do
-  logInfo m!"{repr (← reifyIntExpr ``intNeg)}"
-
-/-- info: some (Lean.Grind.CommRing.Expr.pow (Lean.Grind.CommRing.Expr.num 2) 3) -/
-#guard_msgs in
-run_meta SymM.run do runTestOnInt do
-  logInfo m!"{repr (← reifyIntExpr ``intPow)}"
-
-/--
-info: some (Lean.Grind.CommRing.Expr.sub (Lean.Grind.CommRing.Expr.num 7) (Lean.Grind.CommRing.Expr.num 2))
--/
-#guard_msgs in
-run_meta SymM.run do runTestOnInt do
-  logInfo m!"{repr (← reifyIntExpr ``intSub)}"
-
--- skipVar test: a non-arithmetic term returns none with skipVar=true
-/-- info: none -/
-#guard_msgs in
-run_meta SymM.run do runTestOnInt do
-  let a ← mkFreshExprMVar (mkConst ``Int)
-  logInfo m!"{repr (← reifyRing? a)}"
-
--- skipVar=false: a non-arithmetic term becomes a variable
-/-- info: some (Lean.Grind.CommRing.Expr.var 0) -/
-#guard_msgs in
-run_meta SymM.run do runTestOnInt do
-  let a ← mkFreshExprMVar (mkConst ``Int)
-  logInfo m!"{repr (← reifyRing? a (skipVar := false))}"
-
-opaque a : Int
-opaque b : Int
-opaque c : Int
-def e := (a + b*2) - (c*a + a*(3*b + c))
-
-/--
-info: some (Lean.Grind.CommRing.Expr.sub
-  (Lean.Grind.CommRing.Expr.add
-    (Lean.Grind.CommRing.Expr.var 0)
-    (Lean.Grind.CommRing.Expr.mul (Lean.Grind.CommRing.Expr.var 1) (Lean.Grind.CommRing.Expr.num 2)))
-  (Lean.Grind.CommRing.Expr.add
-    (Lean.Grind.CommRing.Expr.mul (Lean.Grind.CommRing.Expr.var 2) (Lean.Grind.CommRing.Expr.var 0))
-    (Lean.Grind.CommRing.Expr.mul
-      (Lean.Grind.CommRing.Expr.var 0)
-      (Lean.Grind.CommRing.Expr.add
-        (Lean.Grind.CommRing.Expr.mul (Lean.Grind.CommRing.Expr.num 3) (Lean.Grind.CommRing.Expr.var 1))
-        (Lean.Grind.CommRing.Expr.var 2)))))
----
-info: #[a, b, c]
--/
-#guard_msgs in
-run_meta SymM.run do runTestOnInt do
-  logInfo m!"{repr (← reifyIntExpr ``e)}"
-  logInfo (← get).vars
-
-/-! ## Roundtrip tests: reify then denote -/
-
-/-- Reify an expression, denote it back, and check they're definitionally equal. -/
-def roundtrip (n : Name) : TestM Unit := do
-  let orig ← canonExpr (← getDefValue n)
-  let some re ← reifyRing? orig (skipVar := false) | throwError "reify failed"
-  let vars := (← get).vars
-  let denoted ← denoteRingExpr vars re
-  let denoted ← canonExpr denoted
-  unless (← isDefEq orig denoted) do
-    logInfo m!"MISMATCH for {n}:\n  orig:    {orig}\n  denoted: {denoted}"
-    return
-  logInfo m!"roundtrip OK: {n}: {denoted}"
-
-/--
-info: roundtrip OK: intAdd: 2 + 3
----
-info: roundtrip OK: intMulAdd: 2 * 3 + 1
----
-info: roundtrip OK: intNeg: -5
----
-info: roundtrip OK: intPow: 2 ^ 3
----
-info: roundtrip OK: intSub: 7 - 2
----
-info: roundtrip OK: e: a + b * 2 - (c * a + a * (3 * b + c))
--/
-#guard_msgs in
-run_meta SymM.run do runTestOnInt do
-  roundtrip ``intAdd
-  roundtrip ``intMulAdd
-  roundtrip ``intNeg
-  roundtrip ``intPow
-  roundtrip ``intSub
-  roundtrip ``e

tests/elab/timeAPI.lean

@@ -629,9 +629,9 @@ Std.Time.Weekday.friday
   println! repr date.weekOfYear
   println! repr date.weekOfMonth
 
-  println! date.toAmericanDateString
-  println! date.toLeanDateString
-  println! date.toSQLDateString
+  println! (date.format "MM-dd-uuuu")
+  println! (date.format "uuuu-MM-dd")
+  println! (date.format "uuuu-MM-dd")
 
   println! date.toDaysSinceUNIXEpoch
   println! date.toTimestampAssumingUTC

tests/elab/timeCanonFormats.lean

@@ -8,7 +8,7 @@ def date₁ := zoned("2014-06-16T03:03:03-03:00")
 info: "Monday, June 16, 2014 06:03:03"
 -/
 #guard_msgs in
-#eval Formats.longDateFormat.format date₁.toDateTime
+#eval Formats.longDateFormat.format date₁
 
 def tm := date₁.toTimestamp
 def date₂ := DateTime.ofTimestamp tm brTZ
@@ -134,7 +134,7 @@ info: "Mon, 16 Jun 2014 03:03:03 -0300"
 #eval Formats.rfc822.format date₂
 
 /--
-info: "Mon, 16-06-2014 03:03:03 -0300"
+info: "Mon, 16-Jun-14 03:03:03 -0300"
 -/
 #guard_msgs in
 #eval Formats.rfc850.format date₂

tests/elab/timeFieldSymbols.lean

@@ -0,0 +1,833 @@
+import Std.Time
+open Std.Time
+
+-- Reference date: Sunday, July 14, 2002 23:13:12.324354679 UTC+09:00 (Q3, week 28, day 195)
+def td := zoned("2002-07-14T23:13:12.324354679+09:00")
+
+-- Same date/time at UTC (for UTC timezone name tests)
+def tdUTC := zoned("2002-07-14T23:13:12.324354679+00:00")
+
+-- AM hour (09:13:12 for AM/PM tests)
+def tdAM := zoned("2002-07-14T09:13:12.000000000+09:00")
+
+-- Exact noon and midnight (for day-period tests)
+def tdNoon := zoned("2002-07-14T12:00:00.000000000+09:00")
+def tdMidnight := zoned("2002-07-14T00:00:00.000000000+09:00")
+def tdWeekMonth := zoned("2002-08-05T23:13:12.324354679+09:00")
+
+-- Named timezone (for z/V name tests)
+def tokyoTZ : TimeZone := { offset := { second := 32400 }, name := "Asia/Tokyo", abbreviation := "JST", isDST := false }
+
+def tdNamed := ZonedDateTime.ofPlainDateTime td.toPlainDateTime (TimeZone.ZoneRules.ofTimeZone tokyoTZ)
+
+-- Week-based year boundary: Dec 31, 2018 is in ISO week 1 of 2019
+def tdWeekBound := ZonedDateTime.ofPlainDateTime datetime("2018-12-31T12:00:00") (TimeZone.ZoneRules.ofTimeZone TimeZone.UTC)
+
+-- Additional week-based year boundary cases
+-- Jan 1, 2017 (Sunday) → ISO week 52 of 2016
+def tdWeekBound2 := ZonedDateTime.ofPlainDateTime datetime("2017-01-01T12:00:00") (TimeZone.ZoneRules.ofTimeZone TimeZone.UTC)
+-- Jan 2, 2017 (Monday) → ISO week 1 of 2017
+def tdWeekBound3 := ZonedDateTime.ofPlainDateTime datetime("2017-01-02T12:00:00") (TimeZone.ZoneRules.ofTimeZone TimeZone.UTC)
+-- Dec 31, 2019 (Tuesday) → ISO week 1 of 2020
+def tdWeekBound4 := ZonedDateTime.ofPlainDateTime datetime("2019-12-31T12:00:00") (TimeZone.ZoneRules.ofTimeZone TimeZone.UTC)
+-- Jan 1, 2021 (Friday) → ISO week 53 of 2020
+def tdWeekBound5 := ZonedDateTime.ofPlainDateTime datetime("2021-01-01T12:00:00") (TimeZone.ZoneRules.ofTimeZone TimeZone.UTC)
+-- Jan 4, 2021 (Monday) → ISO week 1 of 2021
+def tdWeekBound6 := ZonedDateTime.ofPlainDateTime datetime("2021-01-04T12:00:00") (TimeZone.ZoneRules.ofTimeZone TimeZone.UTC)
+
+-- Jan 1 (day 1) for D zero-padding tests
+def tdJan1 := zoned("2002-01-01T12:00:00.000000000+09:00")
+
+-- Exact noon/midnight with sub-second nanos (b bug fix verification)
+def tdNoonNano     := zoned("2002-07-14T12:00:00.000000001+09:00")
+def tdMidnightNano := zoned("2002-07-14T00:00:00.000000001+09:00")
+
+-- Small fractional-second values (S truncation fix verification)
+-- 10ms = 10_000_000 ns  →  "010..." not "100..."
+def tdTenMs  := zoned("2002-07-14T23:13:12.010000000+09:00")
+-- 1ms = 1_000_000 ns   →  "001..."
+def tdOneMs  := zoned("2002-07-14T23:13:12.001000000+09:00")
+-- 1ns = 1 ns           →  "000000001"
+def tdOneNs  := zoned("2002-07-14T23:13:12.000000001+09:00")
+
+-- PlainTime values for b-on-PlainTime tests
+def ptNoon         := time("12:00:00.000000000")
+def ptMidnight     := time("00:00:00.000000000")
+def ptAM           := time("09:13:12.000000000")
+def ptPM           := time("23:13:12.000000000")
+def ptNoonNano     := time("12:00:00.000000001")
+def ptMidnightNano := time("00:00:00.000000001")
+
+-- Aligned week-of-month edge cases: Aug 1/4/5/11/12 2002
+def tdAug1  := zoned("2002-08-01T12:00:00.000000000+09:00")  -- Thu, W=1
+def tdAug4  := zoned("2002-08-04T12:00:00.000000000+09:00")  -- Sun, W=1
+def tdAug12 := zoned("2002-08-12T12:00:00.000000000+09:00")  -- Mon, W=3
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- G  Era
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "AD AD AD Anno Domini A"
+-/
+#guard_msgs in
+#eval td.format "G GG GGG GGGG GGGGG"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- y  Year of era
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "2002 02 2002 02002 000002002"
+-/
+#guard_msgs in
+#eval td.format "y yy yyyy yyyyy yyyyyyyyy"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- Y  Week-based year
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "2002 02 2002 02002 000002002"
+-/
+#guard_msgs in
+#eval td.format "Y YY YYYY YYYYY YYYYYYYYY"
+
+-- Boundary: Dec 31, 2018 belongs to ISO week 1 of 2019
+/--
+info: "2019 19 2019"
+-/
+#guard_msgs in
+#eval tdWeekBound.format "Y YY YYYY"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- u  Extended year (signed, no era flip)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "2002 02 2002 02002 000002002"
+-/
+#guard_msgs in
+#eval td.format "u uu uuuu uuuuu uuuuuuuuu"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- Q / q  Quarter (Q = formatting, q = standalone — same output here)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "3 03 Q3 3rd quarter 3"
+-/
+#guard_msgs in
+#eval td.format "Q QQ QQQ QQQQ QQQQQ"
+
+/--
+info: "3 03 Q3 3rd quarter 3"
+-/
+#guard_msgs in
+#eval td.format "q qq qqq qqqq qqqqq"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- M / L  Month (M = formatting, L = standalone — same output here)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "7 07 Jul July J"
+-/
+#guard_msgs in
+#eval td.format "M MM MMM MMMM MMMMM"
+
+/--
+info: "7 07 Jul July J"
+-/
+#guard_msgs in
+#eval td.format "L LL LLL LLLL LLLLL"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- w  Week of week-based year
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "28 28"
+-/
+#guard_msgs in
+#eval td.format "w ww"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- W  Week of month (Monday-first)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "2"
+-/
+#guard_msgs in
+#eval td.format "W"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- d  Day of month
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "14 14"
+-/
+#guard_msgs in
+#eval td.format "d dd"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- D  Day of year
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "195 195 195"
+-/
+#guard_msgs in
+#eval td.format "D DD DDD"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- F  Day-of-week-in-month / occurrence within the month
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "2"
+-/
+#guard_msgs in
+#eval td.format "F"
+
+/--
+info: "1 1"
+-/
+#guard_msgs in
+#eval tdWeekMonth.format "W F"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- E  Day of week (text only)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "Sun Sun Sun Sunday S"
+-/
+#guard_msgs in
+#eval td.format "E EE EEE EEEE EEEEE"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- e  Localized day of week (count 1-2 = numeric ordinal, 3-5 = text)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "7 07 Sun Sunday S"
+-/
+#guard_msgs in
+#eval td.format "e ee eee eeee eeeee"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- c  Standalone day of week (count 1 = numeric, 3-5 = text)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "7 Sun Sunday S"
+-/
+#guard_msgs in
+#eval td.format "c ccc cccc ccccc"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- a  AM/PM marker (counts 1-3 = short, 4 = full, 5 = narrow)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "PM"
+-/
+#guard_msgs in
+#eval td.format "a"
+
+/--
+info: "AM"
+-/
+#guard_msgs in
+#eval tdAM.format "a"
+
+/--
+info: "PM PM PM PM p"
+-/
+#guard_msgs in
+#eval td.format "a aa aaa aaaa aaaaa"
+
+/--
+info: "AM AM AM AM a"
+-/
+#guard_msgs in
+#eval tdAM.format "a aa aaa aaaa aaaaa"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- b  Day period (counts 1-3 = short, 4 = full, 5 = narrow)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "PM PM PM PM p"
+-/
+#guard_msgs in
+#eval td.format "b bb bbb bbbb bbbbb"
+
+/--
+info: "AM AM AM AM a"
+-/
+#guard_msgs in
+#eval tdAM.format "b bb bbb bbbb bbbbb"
+
+/--
+info: "noon noon noon noon n"
+-/
+#guard_msgs in
+#eval tdNoon.format "b bb bbb bbbb bbbbb"
+
+/--
+info: "midnight midnight midnight midnight mi"
+-/
+#guard_msgs in
+#eval tdMidnight.format "b bb bbb bbbb bbbbb"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- H  Hour of day (0-23)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "23 23"
+-/
+#guard_msgs in
+#eval td.format "H HH"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- h  Clock hour of AM/PM (1-12)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "11 11"
+-/
+#guard_msgs in
+#eval td.format "h hh"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- K  Hour of AM/PM (0-11)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "11 11"
+-/
+#guard_msgs in
+#eval td.format "K KK"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- k  Clock hour of day (1-24)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "23 23"
+-/
+#guard_msgs in
+#eval td.format "k kk"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- m  Minute
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "13 13"
+-/
+#guard_msgs in
+#eval td.format "m mm"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- s  Second
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "12 12"
+-/
+#guard_msgs in
+#eval td.format "s ss"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- S  Fractional seconds (truncated from nanoseconds)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "3 32 324 3243 324354679"
+-/
+#guard_msgs in
+#eval td.format "S SS SSS SSSS SSSSSSSSS"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- A  Milliseconds since midnight
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "83592324 83592324 83592324 83592324 083592324"
+-/
+#guard_msgs in
+#eval td.format "A AA AAA AAAA AAAAAAAAA"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- n  Nanosecond (Lean/Java extension; minimum width, no truncation)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "324354679 324354679 324354679 324354679 324354679"
+-/
+#guard_msgs in
+#eval td.format "n nn nnn nnnn nnnnnnnnn"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- N  Nanoseconds since midnight (Lean/Java extension; minimum width, no truncation)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "83592324354679 83592324354679 83592324354679 83592324354679 83592324354679"
+-/
+#guard_msgs in
+#eval td.format "N NN NNN NNNN NNNNNNNNN"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- z  Time zone name (short = abbreviation/id, full = long name)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "+09:00 +09:00 +09:00 +09:00"
+-/
+#guard_msgs in
+#eval td.format "z zz zzz zzzz"
+
+/--
+info: "UTC UTC UTC Coordinated Universal Time"
+-/
+#guard_msgs in
+#eval tdUTC.format "z zz zzz zzzz"
+
+/--
+info: "JST JST JST Asia/Tokyo"
+-/
+#guard_msgs in
+#eval tdNamed.format "z zz zzz zzzz"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- Z  Zone offset
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "+0900 +0900 +0900 GMT+09:00 +09:00"
+-/
+#guard_msgs in
+#eval td.format "Z ZZ ZZZ ZZZZ ZZZZZ"
+
+/--
+info: "+0000 +0000 +0000 GMT Z"
+-/
+#guard_msgs in
+#eval tdUTC.format "Z ZZ ZZZ ZZZZ ZZZZZ"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- O  Localized GMT offset
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "GMT+9 GMT+09:00"
+-/
+#guard_msgs in
+#eval td.format "O OOOO"
+
+/--
+info: "GMT GMT"
+-/
+#guard_msgs in
+#eval tdUTC.format "O OOOO"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- V  Zone ID (`VV` only; other widths rejected to match Java)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "+09:00"
+-/
+#guard_msgs in
+#eval td.format "VV"
+
+-- UTC offset-only zone: raw "+00:00", not normalized to "UTC"
+/--
+info: "+00:00"
+-/
+#guard_msgs in
+#eval tdUTC.format "VV"
+
+/--
+info: "Asia/Tokyo"
+-/
+#guard_msgs in
+#eval tdNamed.format "VV"
+
+/--
+info: "error: offset 1: invalid quantity of characters for 'V': must be 2"
+-/
+#guard_msgs in
+#eval td.format "V"
+
+/--
+info: "error: offset 3: invalid quantity of characters for 'V': must be 2"
+-/
+#guard_msgs in
+#eval td.format "VVV"
+
+/--
+info: "error: offset 4: invalid quantity of characters for 'V': must be 2"
+-/
+#guard_msgs in
+#eval td.format "VVVV"
+
+/--
+info: "error: offset 3: invalid quantity of characters for 'd'"
+-/
+#guard_msgs in
+#eval td.format "ddd"
+
+/--
+info: "error: offset 3: invalid quantity of characters for 'w'"
+-/
+#guard_msgs in
+#eval td.format "www"
+
+/--
+info: "error: offset 2: invalid quantity of characters for 'W'"
+-/
+#guard_msgs in
+#eval td.format "WW"
+
+/--
+info: "error: offset 2: invalid quantity of characters for 'F'"
+-/
+#guard_msgs in
+#eval td.format "FF"
+
+/--
+info: "Su"
+-/
+#guard_msgs in
+#eval td.format "EEEEEE"
+
+/--
+info: "Su"
+-/
+#guard_msgs in
+#eval td.format "eeeeee"
+
+/--
+info: "error: offset 2: invalid quantity of characters for 'c'"
+-/
+#guard_msgs in
+#eval td.format "cc"
+
+/--
+info: "Su"
+-/
+#guard_msgs in
+#eval td.format "cccccc"
+
+/--
+info: "error: offset 6: invalid quantity of characters for 'a'"
+-/
+#guard_msgs in
+#eval td.format "aaaaaa"
+
+/--
+info: "error: offset 3: invalid quantity of characters for 'H'"
+-/
+#guard_msgs in
+#eval td.format "HHH"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- v  Generic timezone name (no DST distinction; short = abbreviation, full = name)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+-- offset-only zone: short = raw offset, full = raw offset (same as z)
+/--
+info: "+09:00 +09:00"
+-/
+#guard_msgs in
+#eval td.format "v vvvv"
+
+-- UTC offset-only: normalized to "UTC"/"Coordinated Universal Time" (same as z)
+/--
+info: "UTC Coordinated Universal Time"
+-/
+#guard_msgs in
+#eval tdUTC.format "v vvvv"
+
+-- named zone: short = abbreviation, full = IANA name
+/--
+info: "JST Asia/Tokyo"
+-/
+#guard_msgs in
+#eval tdNamed.format "v vvvv"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- X  ISO 8601 offset (uses Z for UTC)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "+09 +0900 +09:00 +0900 +09:00"
+-/
+#guard_msgs in
+#eval td.format "X XX XXX XXXX XXXXX"
+
+/--
+info: "Z Z Z Z Z"
+-/
+#guard_msgs in
+#eval tdUTC.format "X XX XXX XXXX XXXXX"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- x  ISO 8601 offset (no Z for UTC)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "+09 +0900 +09:00 +0900 +09:00"
+-/
+#guard_msgs in
+#eval td.format "x xx xxx xxxx xxxxx"
+
+/--
+info: "+00 +0000 +00:00 +0000 +00:00"
+-/
+#guard_msgs in
+#eval tdUTC.format "x xx xxx xxxx xxxxx"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- Y  Week-based year: extended boundary cases
+-- ─────────────────────────────────────────────────────────────────────────────
+
+-- Jan 1, 2017 is Sunday → belongs to ISO week 52 of 2016
+/--
+info: "2016 16 2016"
+-/
+#guard_msgs in
+#eval tdWeekBound2.format "Y YY YYYY"
+
+-- Jan 2, 2017 is Monday → first day of ISO week 1 of 2017
+/--
+info: "2017 17 2017"
+-/
+#guard_msgs in
+#eval tdWeekBound3.format "Y YY YYYY"
+
+-- Dec 31, 2019 is Tuesday → belongs to ISO week 1 of 2020
+/--
+info: "2020 20 2020"
+-/
+#guard_msgs in
+#eval tdWeekBound4.format "Y YY YYYY"
+
+-- Jan 1, 2021 is Friday → belongs to ISO week 53 of 2020
+/--
+info: "2020 20 2020"
+-/
+#guard_msgs in
+#eval tdWeekBound5.format "Y YY YYYY"
+
+-- Jan 4, 2021 is Monday → first day of ISO week 1 of 2021
+/--
+info: "2021 21 2021"
+-/
+#guard_msgs in
+#eval tdWeekBound6.format "Y YY YYYY"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- w  Week of year paired with Y: check they agree at boundaries
+-- ─────────────────────────────────────────────────────────────────────────────
+
+-- Jan 1, 2017 → Y=2016 w=52
+/--
+info: "2016 52"
+-/
+#guard_msgs in
+#eval tdWeekBound2.format "Y w"
+
+-- Jan 2, 2017 → Y=2017 w=1
+/--
+info: "2017 1"
+-/
+#guard_msgs in
+#eval tdWeekBound3.format "Y w"
+
+-- Dec 31, 2019 → Y=2020 w=1
+/--
+info: "2020 1"
+-/
+#guard_msgs in
+#eval tdWeekBound4.format "Y w"
+
+-- Jan 1, 2021 → Y=2020 w=53
+/--
+info: "2020 53"
+-/
+#guard_msgs in
+#eval tdWeekBound5.format "Y w"
+
+-- Jan 4, 2021 → Y=2021 w=1
+/--
+info: "2021 1"
+-/
+#guard_msgs in
+#eval tdWeekBound6.format "Y w"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- D  Day of year: zero-padding with count 1/2/3 for day 1
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "1 01 001"
+-/
+#guard_msgs in
+#eval tdJan1.format "D DD DDD"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- W  Aligned week-of-month: Java ALIGNED_WEEK_OF_MONTH = (dayOfMonth-1)/7+1
+-- ─────────────────────────────────────────────────────────────────────────────
+
+-- Aug 1 (Thu): (1-1)/7+1 = 1 → W=1
+/--
+info: "1"
+-/
+#guard_msgs in
+#eval tdAug1.format "W"
+
+-- Aug 4 (Sun): (4-1)/7+1 = 1 → W=1
+/--
+info: "1"
+-/
+#guard_msgs in
+#eval tdAug4.format "W"
+
+-- Aug 5 (Mon): (5-1)/7+1 = 1 → W=1
+/--
+info: "1"
+-/
+#guard_msgs in
+#eval tdWeekMonth.format "W"
+
+-- Aug 12 (Mon): (12-1)/7+1 = 2 → W=2
+/--
+info: "2"
+-/
+#guard_msgs in
+#eval tdAug12.format "W"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- h / K / k  Hour edge cases: midnight (H=0) and noon (H=12)
+-- ─────────────────────────────────────────────────────────────────────────────
+
+-- midnight: H=0, h=12, K=0, k=24
+/--
+info: "0 12 0 24"
+-/
+#guard_msgs in
+#eval tdMidnight.format "H h K k"
+
+-- noon: H=12, h=12, K=0, k=12
+/--
+info: "12 12 0 12"
+-/
+#guard_msgs in
+#eval tdNoon.format "H h K k"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- S  Fractional seconds: truncation for values < 10^8 nanoseconds
+-- ─────────────────────────────────────────────────────────────────────────────
+
+-- 10ms = 10_000_000 ns → left-pad to 9 → "010000000"
+/--
+info: "0 01 010 0100 010000000"
+-/
+#guard_msgs in
+#eval tdTenMs.format "S SS SSS SSSS SSSSSSSSS"
+
+-- 1ms = 1_000_000 ns → "001000000"
+/--
+info: "0 00 001 0010 001000000"
+-/
+#guard_msgs in
+#eval tdOneMs.format "S SS SSS SSSS SSSSSSSSS"
+
+-- 1ns → "000000001"
+/--
+info: "0 00 000 0000 000000001"
+-/
+#guard_msgs in
+#eval tdOneNs.format "S SS SSS SSSS SSSSSSSSS"
+
+-- zero nanoseconds → "000000000"
+/--
+info: "0 00 000 0000 000000000"
+-/
+#guard_msgs in
+#eval tdNoon.format "S SS SSS SSSS SSSSSSSSS"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- b  Day period: nanoseconds prevent noon/midnight classification
+-- ─────────────────────────────────────────────────────────────────────────────
+
+-- 12:00:00.000000001 → PM, not noon (non-zero nanosecond)
+/--
+info: "PM"
+-/
+#guard_msgs in
+#eval tdNoonNano.format "b"
+
+-- 00:00:00.000000001 → AM, not midnight
+/--
+info: "AM"
+-/
+#guard_msgs in
+#eval tdMidnightNano.format "b"
+
+-- exact noon and midnight still work
+/--
+info: "noon midnight"
+-/
+#guard_msgs in
+#eval s!"{tdNoon.format "b"} {tdMidnight.format "b"}"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- b  Day period on PlainTime
+-- ─────────────────────────────────────────────────────────────────────────────
+
+/--
+info: "noon"
+-/
+#guard_msgs in
+#eval ptNoon.format "b"
+
+/--
+info: "midnight"
+-/
+#guard_msgs in
+#eval ptMidnight.format "b"
+
+/--
+info: "AM"
+-/
+#guard_msgs in
+#eval ptAM.format "b"
+
+/--
+info: "PM"
+-/
+#guard_msgs in
+#eval ptPM.format "b"
+
+-- non-zero nano at noon/midnight → falls back to AM/PM
+/--
+info: "PM"
+-/
+#guard_msgs in
+#eval ptNoonNano.format "b"
+
+/--
+info: "AM"
+-/
+#guard_msgs in
+#eval ptMidnightNano.format "b"

tests/elab/timeFormats.lean

@@ -1,17 +1,17 @@
 import Std.Time
 open Std.Time
 
-def RFC1123 : GenericFormat .any := datespec("eee, dd MMM uuuu HH:mm:ss ZZZ")
-def ShortDate : GenericFormat .any := datespec("MM/dd/uuuu")
-def LongDate : GenericFormat .any := datespec("MMMM D, uuuu")
-def ShortDateTime : GenericFormat .any := datespec("MM/dd/uuuu HH:mm:ss")
-def LongDateTime : GenericFormat .any := datespec("MMMM D, uuuu h:mm aa")
-def Time24Hour : GenericFormat .any := datespec("HH:mm:ss")
-def Time12Hour : GenericFormat .any := datespec("hh:mm:ss aa")
-def FullDayTimeZone : GenericFormat .any := datespec("EEEE, MMMM dd, uuuu HH:mm:ss ZZZ")
-def CustomDayTime : GenericFormat .any := datespec("EEE dd MMM uuuu HH:mm")
-def EraDate : GenericFormat .any := datespec("MM D, uuuu G")
-def DateSmall : GenericFormat .any := datespec("uu-MM-dd")
+def RFC1123 : Format Awareness.any := datespec("eee, dd MMM uuuu HH:mm:ss ZZZ")
+def ShortDate : Format Awareness.any := datespec("MM/dd/uuuu")
+def LongDate : Format Awareness.any := datespec("MMMM D, uuuu")
+def ShortDateTime : Format Awareness.any := datespec("MM/dd/uuuu HH:mm:ss")
+def LongDateTime : Format Awareness.any := datespec("MMMM D, uuuu h:mm a")
+def Time24Hour : Format Awareness.any := datespec("HH:mm:ss")
+def Time12Hour : Format Awareness.any := datespec("hh:mm:ss a")
+def FullDayTimeZone : Format Awareness.any := datespec("EEEE, MMMM dd, uuuu HH:mm:ss ZZZ")
+def CustomDayTime : Format Awareness.any := datespec("EEE dd MMM uuuu HH:mm")
+def EraDate : Format Awareness.any := datespec("MM D, uuuu G")
+def DateSmall : Format Awareness.any := datespec("uu-MM-dd")
 
 -- Dates
 
@@ -27,7 +27,7 @@ def time₂ := time("03:11:01")
 info: "Monday, June 16, 2014 03:03:03 -0300"
 -/
 #guard_msgs in
-#eval FullDayTimeZone.format date₁.toDateTime
+#eval FullDayTimeZone.format date₁
 
 def tm := date₁.toTimestamp
 def date₂ := DateTime.ofTimestamp tm brTZ
@@ -197,13 +197,13 @@ info: "03:11:01 AM"
 info: "2024-08-15T14:03:47-03:00"
 -/
 #guard_msgs in
-#eval dateBR₁.toISO8601String
+#eval Formats.iso8601.format dateBR₁
 
 /--
 info: "2024-08-15T14:03:47Z"
 -/
 #guard_msgs in
-#eval dateUTC₁.toISO8601String
+#eval Formats.iso8601.format dateUTC₁
 
 /--
 info: "06/16/2014"
@@ -297,7 +297,7 @@ def tz : TimeZone := { offset := { second := -3600 }, name := "America/Sao_Paulo
 def zoned₆ := ZonedDateTime.ofPlainDateTime (zoned₄.toPlainDateTime) (TimeZone.ZoneRules.ofTimeZone tz)
 
 /--
-info: "CE CE CE Common Era C"
+info: "AD AD AD Anno Domini A"
 -/
 #guard_msgs in
 #eval zoned₄.format "G GG GGG GGGG GGGGG"
@@ -321,10 +321,10 @@ info: "195 195 195"
 #eval zoned₄.format "D DD DDD"
 
 /--
-info: "14 14 014 0014 00014"
+info: "14 14"
 -/
 #guard_msgs in
-#eval zoned₄.format "d dd ddd dddd ddddd"
+#eval zoned₄.format "d dd"
 
 /--
 info: "7 07 Jul July J"
@@ -339,16 +339,16 @@ info: "3 03 3rd quarter 3"
 #eval zoned₄.format "Q QQ QQQQ QQQQQ"
 
 /--
-info: "28 28 028 0028"
+info: "28 28"
 -/
 #guard_msgs in
-#eval zoned₄.format "w ww www wwww"
+#eval zoned₄.format "w ww"
 
 /--
-info: "2 02 002 0002"
+info: "2"
 -/
 #guard_msgs in
-#eval zoned₄.format "W WW WWW WWWW"
+#eval zoned₄.format "W"
 
 /--
 info: "Sun Sun Sun Sunday S"
@@ -363,46 +363,46 @@ info: "7 07 Sun Sunday S"
 #eval zoned₄.format "e ee eee eeee eeeee"
 
 /--
-info: "2 02 002 0002"
+info: "2"
 -/
 #guard_msgs in
-#eval zoned₄.format "F FF FFF FFFF"
+#eval zoned₄.format "F"
 
 /--
-info: "11 11 011 0011 0011"
+info: "11 11"
 -/
 #guard_msgs in
-#eval zoned₄.format "h hh hhh hhhh hhhh"
+#eval zoned₄.format "h hh"
 
 /--
-info: "11 11 011 0011 000011"
+info: "11 11"
 -/
 #guard_msgs in
-#eval zoned₄.format "K KK KKK KKKK KKKKKK"
+#eval zoned₄.format "K KK"
 
 /--
-info: "23 23 023 0023 000023"
+info: "23 23"
 -/
 #guard_msgs in
-#eval zoned₄.format "k kk kkk kkkk kkkkkk"
+#eval zoned₄.format "k kk"
 
 /--
-info: "23 23 023 0023 00023"
+info: "23 23"
 -/
 #guard_msgs in
-#eval zoned₄.format "H HH HHH HHHH HHHHH"
+#eval zoned₄.format "H HH"
 
 /--
-info: "13 13 013 0013 00013"
+info: "13 13"
 -/
 #guard_msgs in
-#eval zoned₄.format "m mm mmm mmmm mmmmm"
+#eval zoned₄.format "m mm"
 
 /--
-info: "12 12 012 0012 00012"
+info: "12 12"
 -/
 #guard_msgs in
-#eval zoned₄.format "s ss sss ssss sssss"
+#eval zoned₄.format "s ss"
 
 
 /--
@@ -441,7 +441,7 @@ info: "+09:00 +09:00 +09:00 +09:00"
 #eval zoned₄.format "z zz zzzz zzzz"
 
 /--
-info: "+00:00 +00:00 +00:00 +00:00"
+info: "UTC UTC Coordinated Universal Time Coordinated Universal Time"
 -/
 #guard_msgs in
 #eval zoned₅.format "z zz zzzz zzzz"
@@ -483,7 +483,7 @@ info: "+0900 +0900 +0900 GMT+09:00 +09:00"
 #eval zoned₄.format "Z ZZ ZZZ ZZZZ ZZZZZ"
 
 /--
-info: "CE CE CE Common Era C"
+info: "AD AD AD Anno Domini A"
 -/
 #guard_msgs in
 #eval datetime₄.format "G GG GGG GGGG GGGGG"
@@ -513,10 +513,10 @@ info: "7 07 Jul J"
 #eval datetime₄.format "M MM MMM MMMMM"
 
 /--
-info: "14 14 014 0014 00014"
+info: "14 14"
 -/
 #guard_msgs in
-#eval datetime₄.format "d dd ddd dddd ddddd"
+#eval datetime₄.format "d dd"
 
 /--
 info: "7 07 Jul July J"
@@ -525,9 +525,9 @@ info: "7 07 Jul July J"
 #eval datetime₄.format "M MM MMM MMMM MMMMM"
 
 /--
-info: "14 14 0014 0014"
+info: "14 14"
 -/#guard_msgs in
-#eval datetime₄.format "d dd dddd dddd"
+#eval datetime₄.format "d dd"
 
 /--
 info: "3 03 3rd quarter 3"
@@ -536,16 +536,16 @@ info: "3 03 3rd quarter 3"
 #eval datetime₄.format "Q QQ QQQQ QQQQQ"
 
 /--
-info: "28 28 028 0028"
+info: "28 28"
 -/
 #guard_msgs in
-#eval datetime₄.format "w ww www wwww"
+#eval datetime₄.format "w ww"
 
 /--
-info: "2 02 002 0002"
+info: "2"
 -/
 #guard_msgs in
-#eval datetime₄.format "W WW WWW WWWW"
+#eval datetime₄.format "W"
 
 /--
 info: "Sun Sun Sun Sunday S"
@@ -560,46 +560,46 @@ info: "7 07 Sun Sunday S"
 #eval datetime₄.format "e ee eee eeee eeeee"
 
 /--
-info: "2 02 002 0002"
+info: "2"
 -/
 #guard_msgs in
-#eval datetime₄.format "F FF FFF FFFF"
+#eval datetime₄.format "F"
 
 /--
-info: "11 11 011 0011 0011"
+info: "11 11"
 -/
 #guard_msgs in
-#eval datetime₄.format "h hh hhh hhhh hhhh"
+#eval datetime₄.format "h hh"
 
 /--
-info: "11 11 011 0011 000011"
+info: "11 11"
 -/
 #guard_msgs in
-#eval datetime₄.format "K KK KKK KKKK KKKKKK"
+#eval datetime₄.format "K KK"
 
 /--
-info: "23 23 023 0023 000023"
+info: "23 23"
 -/
 #guard_msgs in
-#eval datetime₄.format "k kk kkk kkkk kkkkkk"
+#eval datetime₄.format "k kk"
 
 /--
-info: "23 23 023 0023 00023"
+info: "23 23"
 -/
 #guard_msgs in
-#eval datetime₄.format "H HH HHH HHHH HHHHH"
+#eval datetime₄.format "H HH"
 
 /--
-info: "13 13 013 0013 00013"
+info: "13 13"
 -/
 #guard_msgs in
-#eval datetime₄.format "m mm mmm mmmm mmmmm"
+#eval datetime₄.format "m mm"
 
 /--
-info: "12 12 012 0012 00012"
+info: "12 12"
 -/
 #guard_msgs in
-#eval datetime₄.format "s ss sss ssss sssss"
+#eval datetime₄.format "s ss"
 
 
 /--
@@ -632,41 +632,40 @@ info: "83592324354679 83592324354679 83592324354679 83592324354679 8359232435467
 #eval datetime₄.format "N NN NNN NNNN NNNNNNNNN"
 
 /--
-info: "11 11 011 0011 0011"
+info: "11 11"
 -/
 #guard_msgs in
-#eval time₄.format "h hh hhh hhhh hhhh"
+#eval time₄.format "h hh"
 
 /--
-info: "11 11 011 0011 000011"
+info: "11 11"
 -/
 #guard_msgs in
-#eval time₄.format "K KK KKK KKKK KKKKKK"
+#eval time₄.format "K KK"
 
 /--
-info: "23 23 023 0023 000023"
-
+info: "23 23"
 -/
 #guard_msgs in
-#eval time₄.format "k kk kkk kkkk kkkkkk"
+#eval time₄.format "k kk"
 
 /--
-info: "23 23 023 0023 00023"
+info: "23 23"
 -/
 #guard_msgs in
-#eval time₄.format "H HH HHH HHHH HHHHH"
+#eval time₄.format "H HH"
 
 /--
-info: "13 13 013 0013 00013"
+info: "13 13"
 -/
 #guard_msgs in
-#eval time₄.format "m mm mmm mmmm mmmmm"
+#eval time₄.format "m mm"
 
 /--
-info: "12 12 012 0012 00012"
+info: "12 12"
 -/
 #guard_msgs in
-#eval time₄.format "s ss sss ssss sssss"
+#eval time₄.format "s ss"
 
 
 /--
@@ -699,7 +698,7 @@ info: "83592324354679 83592324354679 83592324354679 83592324354679 8359232435467
 #eval time₄.format "N NN NNN NNNN NNNNNNNNN"
 
 /--
-info: "CE CE CE Common Era C"
+info: "AD AD AD Anno Domini A"
 -/
 #guard_msgs in
 #eval date₄.format "G GG GGG GGGG GGGGG"
@@ -729,10 +728,10 @@ info: "7 07 Jul J"
 #eval date₄.format "M MM MMM MMMMM"
 
 /--
-info: "14 14 014 0014 00014"
+info: "14 14"
 -/
 #guard_msgs in
-#eval date₄.format "d dd ddd dddd ddddd"
+#eval date₄.format "d dd"
 
 /--
 info: "7 07 Jul July J"
@@ -741,9 +740,9 @@ info: "7 07 Jul July J"
 #eval date₄.format "M MM MMM MMMM MMMMM"
 
 /--
-info: "14 14 0014 0014"
+info: "14 14"
 -/#guard_msgs in
-#eval date₄.format "d dd dddd dddd"
+#eval date₄.format "d dd"
 
 /--
 info: "3 03 3rd quarter 3"
@@ -752,16 +751,16 @@ info: "3 03 3rd quarter 3"
 #eval date₄.format "Q QQ QQQQ QQQQQ"
 
 /--
-info: "28 28 028 0028"
+info: "28 28"
 -/
 #guard_msgs in
-#eval date₄.format "w ww www wwww"
+#eval date₄.format "w ww"
 
 /--
-info: "2 02 002 0002"
+info: "2"
 -/
 #guard_msgs in
-#eval date₄.format "W WW WWW WWWW"
+#eval date₄.format "W"
 
 /--
 info: "Sun Sun Sun Sunday S"
@@ -776,19 +775,19 @@ info: "7 07 Sun Sunday S"
 #eval date₄.format "e ee eee eeee eeeee"
 
 /--
-info: "2 02 002 0002"
+info: "2"
 -/
 #guard_msgs in
-#eval date₄.format "F FF FFF FFFF"
+#eval date₄.format "F"
 
 /--
-info: "-2000 2001 BCE"
+info: "-2000 2001 BC"
 -/
 #guard_msgs in
 #eval datetime₅.format "uuuu yyyy G"
 
 /--
-info: "2002 2002 CE"
+info: "2002 2002 AD"
 -/
 #guard_msgs in
 #eval datetime₄.format "uuuu yyyy G"
@@ -825,7 +824,7 @@ info: ("19343232432-01-04T01:04:03.000000000",
 #guard_msgs in
 #eval
   let r := PlainDateTime.mk (PlainDate.ofYearMonthDayClip 19343232432 1 4) (PlainTime.mk 25 64 3 0)
-  let s := r.toLeanDateTimeString
+  let s := r.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSS"
   let r := PlainDateTime.parse s
   (s, r, datetime("1932-01-02T05:04:03.000000000"))
 
@@ -840,7 +839,7 @@ def tuple6Mk (a : f) (b : g) (c : h) (d : i) (e : j) (k : z) := some (a, b, c, d
 Parsing Length Tests
 -/
 
-def uFormat : GenericFormat .any := datespec("u uu uuuu uuuuu")
+def uFormat : Format Awareness.any := datespec("u uu uuuu uuuuu")
 
 #eval do assert! (uFormat.parseBuilder tuple4Mk "1 11 1211 12311" |>.isOk)
 #eval do assert! (uFormat.parseBuilder tuple4Mk "12 11 1211 12311" |>.isOk)
@@ -855,7 +854,7 @@ def uFormat : GenericFormat .any := datespec("u uu uuuu uuuuu")
 #eval do assert! (not <| uFormat.parseBuilder tuple4Mk "1 11 1213 111123" |>.isOk)
 #eval do assert! (not <| uFormat.parseBuilder tuple4Mk "1 367 1211 12311" |>.isOk)
 
-def yFormat : GenericFormat .any := datespec("y yy yyyy yyyyy")
+def yFormat : Format Awareness.any := datespec("y yy yyyy yyyyy")
 
 #eval do assert! (yFormat.parseBuilder tuple4Mk "1 11 1211 12311" |>.isOk)
 #eval do assert! (yFormat.parseBuilder tuple4Mk "12 11 1211 12311" |>.isOk)
@@ -870,7 +869,7 @@ def yFormat : GenericFormat .any := datespec("y yy yyyy yyyyy")
 #eval do assert! (not <| yFormat.parseBuilder tuple4Mk "1 11 1213 111123" |>.isOk)
 #eval do assert! (not <| yFormat.parseBuilder tuple4Mk "1 367 1211 12311" |>.isOk)
 
-def dFormat : GenericFormat .any := datespec("D DD DDD")
+def dFormat : Format Awareness.any := datespec("D DD DDD")
 
 #eval do assert! (dFormat.parseBuilder tuple3Mk "1 12 123" |>.isOk)
 #eval do assert! (dFormat.parseBuilder tuple3Mk "323 12 123" |>.isOk)
@@ -879,23 +878,23 @@ def dFormat : GenericFormat .any := datespec("D DD DDD")
 #eval do assert! (not <| dFormat.parseBuilder tuple3Mk "1 123 123" |>.isOk)
 #eval do assert! (not <| dFormat.parseBuilder tuple3Mk "367 12 123" |>.isOk)
 
-def dddFormat : GenericFormat .any := datespec("d dd ddd dddd ddddd")
+def dayOfMonthFormat : Format Awareness.any := datespec("d dd")
 
-#eval do assert! (dddFormat.parseBuilder tuple5Mk "1 12 031 0031 00031" |>.isOk)
-#eval do assert! (dddFormat.parseBuilder tuple5Mk "000031 12 031 0031 00031" |>.isOk)
+#eval do assert! (dayOfMonthFormat.parseBuilder tuple2Mk "1 12" |>.isOk)
+#eval do assert! (dayOfMonthFormat.parseBuilder tuple2Mk "31 31" |>.isOk)
 
-#eval do assert! (not <| dddFormat.parseBuilder tuple5Mk "1 12 0031 00031" |>.isOk)
-#eval do assert! (not <| dddFormat.parseBuilder tuple5Mk "1 031 0031 000031" |>.isOk)
+#eval do assert! (not <| dayOfMonthFormat.parseBuilder tuple2Mk "1 123" |>.isOk)
+#eval do assert! (not <| dayOfMonthFormat.parseBuilder tuple2Mk "32 31" |>.isOk)
 
-def wFormat : GenericFormat .any := datespec("w ww www wwww")
+def wFormat : Format Awareness.any := datespec("w ww")
 
-#eval do assert! (wFormat.parseBuilder tuple4Mk "1 01 031 0031" |>.isOk)
-#eval do assert! (wFormat.parseBuilder tuple4Mk "2 01 031 0031" |>.isOk)
+#eval do assert! (wFormat.parseBuilder tuple2Mk "1 01" |>.isOk)
+#eval do assert! (wFormat.parseBuilder tuple2Mk "2 01" |>.isOk)
 
-#eval do assert! (not <| wFormat.parseBuilder tuple4Mk "2 01 031 00310" |>.isOk)
-#eval do assert! (not <| wFormat.parseBuilder tuple4Mk "2 01 031 031" |>.isOk)
+#eval do assert! (not <| wFormat.parseBuilder tuple2Mk "2 031" |>.isOk)
+#eval do assert! (not <| wFormat.parseBuilder tuple2Mk "54 01" |>.isOk)
 
-def qFormat : GenericFormat .any := datespec("q qq")
+def qFormat : Format Awareness.any := datespec("q qq")
 
 #eval do assert! (qFormat.parseBuilder tuple2Mk "1 02" |>.isOk)
 #eval do assert! (qFormat.parseBuilder tuple2Mk "3 03" |>.isOk)
@@ -903,15 +902,14 @@ def qFormat : GenericFormat .any := datespec("q qq")
 #eval do assert! (not <| qFormat.parseBuilder tuple2Mk "12 32" |>.isOk)
 #eval do assert! (not <| qFormat.parseBuilder tuple2Mk "000001 003" |>.isOk)
 
-def WFormat : GenericFormat .any := datespec("W WW")
+def WFormat : Format Awareness.any := datespec("W")
 
-#eval do assert! (WFormat.parseBuilder tuple2Mk "1 06" |>.isOk)
-#eval do assert! (WFormat.parseBuilder tuple2Mk "3 03" |>.isOk)
+#eval do assert! (WFormat.parseBuilder some "1" |>.isOk)
+#eval do assert! (WFormat.parseBuilder some "3" |>.isOk)
 
-#eval do assert! (not <| WFormat.parseBuilder tuple2Mk "12 32" |>.isOk)
-#eval do assert! (not <| WFormat.parseBuilder tuple2Mk "000001 003" |>.isOk)
+#eval do assert! (not <| WFormat.parseBuilder some "12" |>.isOk)
 
-def eFormat : GenericFormat .any := datespec("e ee")
+def eFormat : Format Awareness.any := datespec("e ee")
 
 #eval do assert! (eFormat.parseBuilder tuple2Mk "1 07" |>.isOk)
 #eval do assert! (eFormat.parseBuilder tuple2Mk "3 03" |>.isOk)
@@ -919,15 +917,15 @@ def eFormat : GenericFormat .any := datespec("e ee")
 #eval do assert! (not <| eFormat.parseBuilder tuple2Mk "12 32" |>.isOk)
 #eval do assert! (not <| eFormat.parseBuilder tuple2Mk "000001 003" |>.isOk)
 
-def FFormat : GenericFormat .any := datespec("F FF")
+def FFormat : Format Awareness.any := datespec("F")
 
-#eval do assert! (FFormat.parseBuilder tuple2Mk "1 04" |>.isOk)
-#eval do assert! (FFormat.parseBuilder tuple2Mk "3 03" |>.isOk)
+#eval do assert! (FFormat.parseBuilder some "1" |>.isOk)
+#eval do assert! (FFormat.parseBuilder some "3" |>.isOk)
 
-#eval do assert! (not <| FFormat.parseBuilder tuple2Mk "12 32" |>.isOk)
-#eval do assert! (not <| FFormat.parseBuilder tuple2Mk "000001 003" |>.isOk)
+#eval do assert! (not <| FFormat.parseBuilder some "12" |>.isOk)
+#eval do assert! (not <| FFormat.parseBuilder some "6" |>.isOk)
 
-def hFormat : GenericFormat .any := datespec("h hh")
+def hFormat : Format Awareness.any := datespec("h hh")
 
 #eval do assert! (hFormat.parseBuilder tuple2Mk "1 09" |>.isOk)
 #eval do assert! (hFormat.parseBuilder tuple2Mk "12 12" |>.isOk)
@@ -949,16 +947,16 @@ info: zoned("2002-07-14T14:13:12.000000000+23:59")
 info: Except.error "offset 22: invalid hour offset: 24. Must be between 0 and 23."
 -/
 #guard_msgs in
-#eval ZonedDateTime.fromLeanDateTimeWithZoneString "2002-07-14T14:13:12+24:59"
+#eval Formats.leanDateTimeWithZoneAlt.parse "2002-07-14T14:13:12+24:59"
 
 /--
 info: Except.error "offset 25: invalid minute offset: 60. Must be between 0 and 59."
 -/
 #guard_msgs in
-#eval ZonedDateTime.fromLeanDateTimeWithZoneString "2002-07-14T14:13:12+23:60"
+#eval Formats.leanDateTimeWithZoneAlt.parse "2002-07-14T14:13:12+23:60"
 
 /--
 info: Except.ok (zoned("2002-07-14T14:13:12.000000000Z"))
 -/
 #guard_msgs in
-#eval ZonedDateTime.fromLeanDateTimeWithZoneString "2002-07-14T14:13:12+00:00"
+#eval Formats.leanDateTimeWithZoneAlt.parse "2002-07-14T14:13:12+00:00"

tests/elab/timeIO.lean

@@ -40,9 +40,9 @@ info: 2013-10-19T23:59:59.000000000-03:00
 #guard_msgs in
 #eval do
   let zr ← Database.defaultGetZoneRules "America/Sao_Paulo"
-  println! "{ZonedDateTime.ofPlainDateTime datetime("2013-10-19T23:59:59") zr |>.toLeanDateTimeWithZoneString}"
-  println! "{ZonedDateTime.ofPlainDateTime datetime("2013-10-20T00:00:00") zr |>.toLeanDateTimeWithZoneString}"
-  println! "{ZonedDateTime.ofPlainDateTime datetime("2013-10-20T00:00:01") zr |>.toLeanDateTimeWithZoneString}"
+  println! "{ZonedDateTime.ofPlainDateTime datetime("2013-10-19T23:59:59") zr |>.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ"}"
+  println! "{ZonedDateTime.ofPlainDateTime datetime("2013-10-20T00:00:00") zr |>.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ"}"
+  println! "{ZonedDateTime.ofPlainDateTime datetime("2013-10-20T00:00:01") zr |>.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ"}"
 
 /-
 Java:
@@ -59,9 +59,9 @@ info: 2019-11-03T01:59:59.000000000-05:00
 #guard_msgs in
 #eval do
   let zr ← Database.defaultGetZoneRules "America/Chicago"
-  println! "{ZonedDateTime.ofPlainDateTime datetime("2019-11-03T01:59:59") zr |>.toLeanDateTimeWithZoneString}"
-  println! "{ZonedDateTime.ofPlainDateTime datetime("2019-11-03T02:00:00") zr |>.toLeanDateTimeWithZoneString}"
-  println! "{ZonedDateTime.ofPlainDateTime datetime("2019-11-03T02:59:59") zr |>.toLeanDateTimeWithZoneString}"
+  println! "{ZonedDateTime.ofPlainDateTime datetime("2019-11-03T01:59:59") zr |>.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ"}"
+  println! "{ZonedDateTime.ofPlainDateTime datetime("2019-11-03T02:00:00") zr |>.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ"}"
+  println! "{ZonedDateTime.ofPlainDateTime datetime("2019-11-03T02:59:59") zr |>.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ"}"
 
 /-
 Java:
@@ -78,6 +78,6 @@ info: 2003-10-26T01:59:59.000000000-05:00
 #guard_msgs in
 #eval do
   let zr ← Database.defaultGetZoneRules "America/Monterrey"
-  println! "{ZonedDateTime.ofPlainDateTime datetime("2003-10-26T01:59:59") zr |>.toLeanDateTimeWithZoneString}"
-  println! "{ZonedDateTime.ofPlainDateTime datetime("2003-10-26T02:00:00") zr |>.toLeanDateTimeWithZoneString}"
-  println! "{ZonedDateTime.ofPlainDateTime datetime("2003-10-26T02:59:59") zr |>.toLeanDateTimeWithZoneString}"
+  println! "{ZonedDateTime.ofPlainDateTime datetime("2003-10-26T01:59:59") zr |>.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ"}"
+  println! "{ZonedDateTime.ofPlainDateTime datetime("2003-10-26T02:00:00") zr |>.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ"}"
+  println! "{ZonedDateTime.ofPlainDateTime datetime("2003-10-26T02:59:59") zr |>.format "uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZZZZZ"}"

tests/elab/timeLimits.lean

@@ -2,9 +2,9 @@ import Std.Time
 open Std.Time
 
 
-def ISO8601UTCAllow : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZ", { allowLeapSeconds := true })
-def ISO8601UTCNot : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZ", { allowLeapSeconds := false })
-def ISO8601UTCDef : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZ")
+def ISO8601UTCAllow : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZ", { allowLeapSeconds := true })
+def ISO8601UTCNot : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZ", { allowLeapSeconds := false })
+def ISO8601UTCDef : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZ")
 
 /--
 info: Except.ok (zoned("2002-07-14T23:14:00.324354679-23:59"))

tests/elab/timeLocalDateTime.lean

@@ -2,8 +2,8 @@ import Std.Time
 import Init
 open Std.Time
 
-def ShortDateTime : GenericFormat .any := datespec("dd/MM/uuuu HH:mm:ss")
-def ShortDate : GenericFormat .any := datespec("dd/MM/uuuu")
+def ShortDateTime : Format Awareness.any := datespec("dd/MM/uuuu HH:mm:ss")
+def ShortDate : Format Awareness.any := datespec("dd/MM/uuuu")
 
 def format (PlainDate : PlainDateTime) : String := ShortDateTime.formatBuilder PlainDate.day PlainDate.month PlainDate.year PlainDate.time.hour PlainDate.minute PlainDate.time.second
 def format₂ (PlainDate : PlainDate) : String := ShortDate.formatBuilder PlainDate.day PlainDate.month PlainDate.year

tests/elab/timeParse.lean

@@ -1,18 +1,18 @@
 import Std.Time
 open Std.Time
 
-def ISO8601UTC : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSXXX")
-def RFC1123 : GenericFormat .any := datespec("eee, dd MMM uuuu HH:mm:ss ZZZ")
-def ShortDate : GenericFormat .any := datespec("MM/dd/uuuu")
-def LongDate : GenericFormat .any := datespec("MMMM D, uuuu")
-def ShortDateTime : GenericFormat .any := datespec("MM/dd/uuuu HH:mm:ss")
-def LongDateTime : GenericFormat .any := datespec("MMMM dd, uuuu hh:mm aa")
-def Time24Hour : GenericFormat .any := datespec("HH:mm:ss")
-def Time12Hour : GenericFormat .any := datespec("hh:mm:ss aa")
-def FullDayTimeZone : GenericFormat .any := datespec("EEEE, MMMM dd, uuuu HH:mm:ss ZZZ")
-def CustomDayTime : GenericFormat .any := datespec("EEE dd MMM uuuu HH:mm")
+def ISO8601UTC : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSXXX")
+def RFC1123 : Format Awareness.any := datespec("eee, dd MMM uuuu HH:mm:ss ZZZ")
+def ShortDate : Format Awareness.any := datespec("MM/dd/uuuu")
+def LongDate : Format Awareness.any := datespec("MMMM D, uuuu")
+def ShortDateTime : Format Awareness.any := datespec("MM/dd/uuuu HH:mm:ss")
+def LongDateTime : Format Awareness.any := datespec("MMMM dd, uuuu hh:mm a")
+def Time24Hour : Format Awareness.any := datespec("HH:mm:ss")
+def Time12Hour : Format Awareness.any := datespec("hh:mm:ss a")
+def FullDayTimeZone : Format Awareness.any := datespec("EEEE, MMMM dd, uuuu HH:mm:ss ZZZ")
+def CustomDayTime : Format Awareness.any := datespec("EEE dd MMM uuuu HH:mm")
 
-def Full12HourWrong : GenericFormat .any := datespec("MM/dd/uuuu hh:mm:ss aa XXX")
+def Full12HourWrong : Format Awareness.any := datespec("MM/dd/uuuu hh:mm:ss a XXX")
 
 -- Dates
 
@@ -30,7 +30,7 @@ info: "2014-06-16T03:03:03.000000100-03:00"
 #guard_msgs in
 #eval
     let t : ZonedDateTime := ISO8601UTC.parse! "2014-06-16T03:03:03.000000100-03:00"
-    ISO8601UTC.format t.toDateTime
+    ISO8601UTC.format t
 
 def tm := date₁.toTimestamp
 def date₂ := DateTime.ofTimestamp tm brTZ
@@ -41,7 +41,7 @@ info: "2014-06-16T03:03:03.000000000-03:00"
 #guard_msgs in
 #eval
     let t : ZonedDateTime := RFC1123.parse! "Mon, 16 Jun 2014 03:03:03 -0300"
-    ISO8601UTC.format t.toDateTime
+    ISO8601UTC.format t
 
 def tm₃ := date₁.toTimestamp
 def date₃ := DateTime.ofTimestamp tm₃ brTZ
@@ -52,7 +52,7 @@ info: "2014-06-16T00:00:00.000000000Z"
 #guard_msgs in
 #eval
     let t : ZonedDateTime := ShortDate.parse! "06/16/2014"
-    ISO8601UTC.format t.toDateTime
+    ISO8601UTC.format t
 
 -- the timestamp is always related to UTC.
 
@@ -73,7 +73,7 @@ info: "2024-08-15T13:28:12.000000000-03:00"
 #guard_msgs in
 #eval
     let t := FullDayTimeZone.parse! "Thursday, August 15, 2024 13:28:12 -0300"
-    ISO8601UTC.format t.toDateTime
+    ISO8601UTC.format t
 
 /--
 info: "2024-08-16T01:28:00.000000000Z"
@@ -81,7 +81,7 @@ info: "2024-08-16T01:28:00.000000000Z"
 #guard_msgs in
 #eval
     let t : ZonedDateTime := LongDateTime.parse! "August 16, 2024 01:28 AM"
-    ISO8601UTC.format t.toDateTime
+    ISO8601UTC.format t
 
 /--
 info: "0000-12-31T22:28:12.000000000+09:00"
@@ -105,7 +105,7 @@ info: "Thu 15 Aug 2024 16:28"
 #guard_msgs in
 #eval
     let t2 : ZonedDateTime := FullDayTimeZone.parse! "Thursday, August 15, 2024 16:28:12 -0000"
-    CustomDayTime.format t2.toDateTime
+    CustomDayTime.format t2
 
 /--
 info: "2024-08-16T13:28:00.000000000Z"
@@ -113,7 +113,7 @@ info: "2024-08-16T13:28:00.000000000Z"
 #guard_msgs in
 #eval
     let t5 : ZonedDateTime := CustomDayTime.parse! "Thu 16 Aug 2024 13:28"
-    ISO8601UTC.format t5.toDateTime
+    ISO8601UTC.format t5
 
 /--
 info: "2024-08-16T01:28:12.000000000+09:00"
@@ -153,7 +153,7 @@ info: "2024-08-15T14:03:47.000000000-03:00"
 #guard_msgs in
 #eval
     let t : ZonedDateTime := FullDayTimeZone.parse! "Thursday, August 15, 2024 14:03:47 -0300"
-    ISO8601UTC.format t.toDateTime
+    ISO8601UTC.format t
 
 /--
 info: "2024-08-15T14:03:47.000000000+09:00"
@@ -161,7 +161,7 @@ info: "2024-08-15T14:03:47.000000000+09:00"
 #guard_msgs in
 #eval
     let t1 : ZonedDateTime := FullDayTimeZone.parse! "Thursday, August 15, 2024 14:03:47 +0900"
-    ISO8601UTC.format t1.toDateTime
+    ISO8601UTC.format t1
 
 /--
 info: "2014-06-16T03:03:03.000000000-03:00"
@@ -169,7 +169,7 @@ info: "2014-06-16T03:03:03.000000000-03:00"
 #guard_msgs in
 #eval
     let t2 : ZonedDateTime := FullDayTimeZone.parse! "Monday, June 16, 2014 03:03:03 -0300"
-    ISO8601UTC.format t2.toDateTime
+    ISO8601UTC.format t2
 
 /--
 info: Except.ok "1993-05-10T10:30:23.000000000+03:00"
@@ -177,7 +177,7 @@ info: Except.ok "1993-05-10T10:30:23.000000000+03:00"
 #guard_msgs in
 #eval
     let t2 := Full12HourWrong.parse "05/10/1993 10:30:23 AM +03:00"
-    (ISO8601UTC.format ·.toDateTime) <$> t2
+    (ISO8601UTC.format ·) <$> t2
 
 /--
 info: Except.ok "1993-05-10T22:30:23.000000000+03:00"
@@ -185,7 +185,7 @@ info: Except.ok "1993-05-10T22:30:23.000000000+03:00"
 #guard_msgs in
 #eval
     let t2 := Full12HourWrong.parse "05/10/1993 10:30:23 PM +03:00"
-    (ISO8601UTC.format ·.toDateTime) <$> t2
+    (ISO8601UTC.format ·) <$> t2
 
 /--
 info: Except.error "offset 13: need a natural number in the interval of 1 to 12"
@@ -193,7 +193,7 @@ info: Except.error "offset 13: need a natural number in the interval of 1 to 12"
 #guard_msgs in
 #eval
     let t2 := Full12HourWrong.parse "05/10/1993 20:30:23 AM +03:00"
-    (ISO8601UTC.format ·.toDateTime) <$> t2
+    (ISO8601UTC.format ·) <$> t2
 
 /--
 info: Except.error "offset 13: need a natural number in the interval of 1 to 12"
@@ -201,4 +201,4 @@ info: Except.error "offset 13: need a natural number in the interval of 1 to 12"
 #guard_msgs in
 #eval
     let t2 := Full12HourWrong.parse "05/10/1993 20:30:23 PM +03:00"
-    (ISO8601UTC.format ·.toDateTime) <$> t2
+    (ISO8601UTC.format ·) <$> t2

tests/elab/timeSet.lean

@@ -1,18 +1,18 @@
 import Std.Time
 open Std.Time
 
-def ISO8601UTC : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSXXX")
-def RFC1123 : GenericFormat .any := datespec("eee, dd MMM uuuu HH:mm:ss ZZZ")
-def ShortDate : GenericFormat .any := datespec("MM/dd/uuuu")
-def LongDate : GenericFormat .any := datespec("MMMM D, uuuu")
-def ShortDateTime : GenericFormat .any := datespec("MM/dd/uuuu HH:mm:ss")
-def LongDateTime : GenericFormat .any := datespec("MMMM dd, uuuu hh:mm aa")
-def Time24Hour : GenericFormat .any := datespec("HH:mm:ss")
-def Time12Hour : GenericFormat .any := datespec("hh:mm:ss aa")
-def FullDayTimeZone : GenericFormat .any := datespec("EEEE, MMMM dd, uuuu HH:mm:ss ZZZ")
-def CustomDayTime : GenericFormat .any := datespec("EEE dd MMM uuuu HH:mm")
+def ISO8601UTC : Format Awareness.any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSXXX")
+def RFC1123 : Format Awareness.any := datespec("eee, dd MMM uuuu HH:mm:ss ZZZ")
+def ShortDate : Format Awareness.any := datespec("MM/dd/uuuu")
+def LongDate : Format Awareness.any := datespec("MMMM D, uuuu")
+def ShortDateTime : Format Awareness.any := datespec("MM/dd/uuuu HH:mm:ss")
+def LongDateTime : Format Awareness.any := datespec("MMMM dd, uuuu hh:mm a")
+def Time24Hour : Format Awareness.any := datespec("HH:mm:ss")
+def Time12Hour : Format Awareness.any := datespec("hh:mm:ss a")
+def FullDayTimeZone : Format Awareness.any := datespec("EEEE, MMMM dd, uuuu HH:mm:ss ZZZ")
+def CustomDayTime : Format Awareness.any := datespec("EEE dd MMM uuuu HH:mm")
 
-def Full12HourWrong : GenericFormat .any := datespec("MM/dd/uuuu hh:mm:ss aa XXX")
+def Full12HourWrong : Format Awareness.any := datespec("MM/dd/uuuu hh:mm:ss a XXX")
 
 -- Dates
 

tests/elab/timeTzifParse.lean

@@ -98,13 +98,13 @@ info: 0
 #eval code.v1.utLocalIndicators.size
 
 /--
-info: zoned("1969-12-31T21:00:00.000000000-03:00")
+info: zoned("1969-12-31T21:00:00.000000000-03:00[America/Sao_Paulo]")
 -/
 #guard_msgs in
 #eval ZonedDateTime.ofTimestamp (Timestamp.ofSecondsSinceUnixEpoch 0) rules
 
 /--
-info: zoned("2012-12-10T00:35:47.000000000-02:00")
+info: zoned("2012-12-10T00:35:47.000000000-02:00[America/Sao_Paulo]")
 -/
 #guard_msgs in
 #eval ZonedDateTime.ofTimestamp (Timestamp.ofSecondsSinceUnixEpoch 1355106947) rules

tests/elab/versoDocs.lean

@@ -241,6 +241,7 @@ error: Unknown constant `b`
 
 Hint: Insert a fully-qualified name:
   • {name ̲(̲f̲u̲l̲l̲ ̲:̲=̲ ̲A̲.̲b̲)̲}`b`
+  • {name ̲(̲f̲u̲l̲l̲ ̲:̲=̲ ̲S̲t̲d̲.̲T̲i̲m̲e̲.̲M̲o̲d̲i̲f̲i̲e̲r̲.̲b̲)̲}`b`
   • {name ̲(̲f̲u̲l̲l̲ ̲:̲=̲ ̲M̲e̲t̲a̲.̲G̲r̲i̲n̲d̲.̲A̲r̲i̲t̲h̲.̲C̲u̲t̲s̲a̲t̲.̲D̲v̲d̲S̲o̲l̲u̲t̲i̲o̲n̲.̲b̲)̲}`b`
 -/
 #guard_msgs in

tests/elab/versoDocs.lean.out.expected

@@ -5,7 +5,7 @@ Nat.gcd.induction' {P : Nat → Nat → Prop} (m n : Nat) (H0 : ∀ (n : Nat), P
   (H1 : ∀ (m n : Nat), 0 < m → P (n % m) m → P m n) : P m n
 something : Unit
 yetMore' : Unit
-versoDocs.lean:631:43-631:53: warning: Code element could be more specific.
+versoDocs.lean:632:43-632:53: warning: Code element could be more specific.
 
 Hint: Insert a role to document it:
   • {̲l̲e̲a̲n̲}̲`-checked`