Commit 2023-09-06 13:50 380bf315

View on Github →

feat(Data/Sum/Basic): create direct versions of get(Left|Right)? analogous to Option.get (#6663)

Estimated changes

added def Sum.getLeft
modified theorem Sum.getLeft?_eq_some_iff
added theorem Sum.getLeft_eq_iff
added theorem Sum.getLeft_inl
added def Sum.getRight
modified theorem Sum.getRight?_eq_some_iff
added theorem Sum.getRight_eq_iff
added theorem Sum.getRight_inr
added theorem Sum.inl_getLeft
added theorem Sum.inr_getRight