option): option_congr (#12263)

Commit

3 years ago

feat(data/equiv/option): option_congr (#12263) This is a universe-polymorphic version of the existing `equiv_functor.map_equiv option`.

Author

eric-wieser

Parents