Commit 2026-01-06 09:05 b79634a5

View on Github →

chore(Data/Option): deprecate Option.iget (#33583) This PR deprecates Option.iget in favor of Option.get! (which will panic on none) or Option.getD (which takes an explicit default value). See [#mathlib4 > `Option.iget` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60Option.2Eiget.60/near/565951044) 🤖 Prepared with Claude Code

Estimated changes

Modified Mathlib/Computability/Primrec.lean

added theorem Primrec.option_getD_default

Modified Mathlib/Computability/TMToPartrec.lean

Modified Mathlib/Computability/TuringMachine.lean

Modified Mathlib/Data/List/Basic.lean

modified theorem List.getLastI_eq_getLast?

added theorem List.getLastI_eq_getLast?_getD

modified theorem List.head!_eq_head?

added theorem List.head!_eq_head?_getD

Modified Mathlib/Data/List/GetD.lean

added theorem List.getI_eq_getElem?_getD

modified theorem List.getI_eq_iget_getElem?

Modified Mathlib/Data/Nat/Digits/Lemmas.lean

Modified Mathlib/Data/Option/Basic.lean

Modified Mathlib/Data/Option/Defs.lean

Modified Mathlib/Logic/Encodable/Basic.lean

added theorem Encodable.surjective_decode_getD

Modified Mathlib/MeasureTheory/Constructions/Pi.lean

Modified Mathlib/MeasureTheory/Function/Jacobian.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Pi.lean

Modified Mathlib/Tactic/CC/Addition.lean