Commit 2023-08-18 21:51 6c6f2a6a

View on Github →

fix(Data/Sum/Basic): Add ? to Sum-get function names. (#6665) As the getLeft and getRight functions are to Option, they should have a ? on the end.

Estimated changes

deleted def Sum.getLeft
added def Sum.getLeft?
added theorem Sum.getLeft?_inl
added theorem Sum.getLeft?_inr
added theorem Sum.getLeft?_map
added theorem Sum.getLeft?_swap
deleted theorem Sum.getLeft_eq_none_iff
deleted theorem Sum.getLeft_eq_some_iff
deleted theorem Sum.getLeft_inl
deleted theorem Sum.getLeft_inr
deleted theorem Sum.getLeft_map
deleted theorem Sum.getLeft_swap
deleted def Sum.getRight
added def Sum.getRight?
added theorem Sum.getRight?_inl
added theorem Sum.getRight?_inr
added theorem Sum.getRight?_map
added theorem Sum.getRight?_swap
deleted theorem Sum.getRight_eq_none_iff
deleted theorem Sum.getRight_eq_some_iff
deleted theorem Sum.getRight_inl
deleted theorem Sum.getRight_inr
deleted theorem Sum.getRight_map
deleted theorem Sum.getRight_swap