Commit 2022-09-15 14:29 559fa0be

View on Github →

chore: remove stuff moved to std4 (#415)

Estimated changes

Modified Mathlib/Data/Option/Basic.lean

deleted theorem Option.lift_or_get_choice

Deleted test/Simpa.lean

deleted def foo