4 ms·
It shoud be possible. A specific feature of Coq that we use is impredicative Set. I do not know if this is the case in F*.
by clarus 2y ago
It shoud be possible. A specific feature of Coq that we use is impredicative Set. I do not know if this is the case in F*.