Created
June 24, 2023 09:41
-
-
Save Octachron/538700cbe49e0eb8e1068c7ed89cd1c8 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
let maybe_reduce | |
(MonoidElement.Constructor ((module Monoid1) as monoid1, element1)) | |
(MonoidElement.Constructor ((module Monoid2) as monoid2, element2)) = | |
let element1_is_unit = Monoid1.eq element1 Monoid1.unit in | |
let element2_is_unit = Monoid2.eq element2 Monoid2.unit in | |
let same_monoid = Type_equal.Id.same_witness Monoid1.t Monoid2.t in | |
match element1_is_unit, element2_is_unit, same_monoid with | |
| true, _, _ -> Reduced (MonoidElement.Constructor (monoid2, element2)) | |
| _, true, _ -> Reduced (MonoidElement.Constructor (monoid1, element1)) | |
| _, _, Some eq -> | |
let element1_in_2 = Type_equal.conv eq element1 in | |
let element = Monoid2.op element1_in_2 element2 in | |
Reduced (MonoidElement.Constructor (monoid2, element)) | |
| false, false, None -> Irreducible |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment