Mathlib v3 is deprecated. Go to Mathlib v4

Def sum.get_right

Modification history

2021-12-31 07:44
src/data/sum/basic.lean
docs(data/sum/basic): Expand module docstring and cleanup (#11158) …
Modified sum.get_rightView on Github →
2020-08-15 16:25
src/data/sum.lean
feat(data/sum): add sum.{get_left, get_right, is_left, is_right} (#3792)
Added sum.get_rightView on Github →