4 ms·
I know the kernel of Hol-Light very well, as I implemented proof terms for it [1]. 600-637 do not define subtypes, but entirely new types. And no, you cannot ad
by practal 5y ago
I know the kernel of Hol-Light very well, as I implemented proof terms for it [1]. 600-637 do not define subtypes, but entirely new types. And no, you cannot add subtypes to a COC prover easily.
[1]: https://link.springer.com/chapter/10.1007/11814771_27 https://link.springer.com/chapter/10.1007/11814771_27