Commit 2025-11-20 14:55 7a60b315

View on Github →

feat: add getD_comp_some lemma for Option type (#31828) Adds a simp lemma that allows this expression to be simplified, even if it isn't applied to an argument. Identified in https://github.com/google-deepmind/formal-conjectures/pull/1120

Estimated changes