3 ms·
I'd be very interested to see an example of an embedded theorem proving system here. My understanding is that unless your language lives and breathes type theor
by tel 12y ago
I'd be very interested to see an example of an embedded theorem proving system here. My understanding is that unless your language lives and breathes type theory you cannot embed a proof system.
- mpweiher 12y agoWell, considering the c2 entry spoke of a dynamically typed language as base, the authors probably meant something more along the lines of SOURL: http://soft.vub.ac.be/SOUL/ http://soft.vub.ac.be/SOUL/