Created
March 7, 2023 09:34
-
-
Save mheiber/b6481a36f1e90da7bb16d004bc75df22 to your computer and use it in GitHub Desktop.
This file contains 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
type (_, _) eq = Eq: ('a, 'a) eq | |
module M: sig | |
type t | |
type u | |
val tx: t | |
val ux: u | |
val eq_t_int: (t, int) eq | |
val eq_int_u: (int, u) eq | |
end = struct | |
type t = int | |
type u = int | |
let tx = 0 | |
let ux = 0 | |
let eq_t_int = Eq | |
let eq_int_u = Eq | |
end | |
let eq_trans : type a b c. (a, b) eq -> (b, c) eq -> (a, c) eq = fun Eq Eq -> Eq | |
let eq_symm : type a b. (a, b) eq -> (b, a) eq = fun Eq -> Eq | |
let convert tx = | |
let Eq = eq_trans M.eq_t_int M.eq_int_u in | |
tx | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment