Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Mike just started explicit mathematics. I added a bit more flesh, but it’s still quite stubby.
Wow, how did you notice that so quickly? I only made a little stub there because Andrej suggested adding a reference to it to Bishop’s constructive mathematics, and I didn’t have time to actually learn anything about it.
Well, I was just looking at Bishop’s constructive mathematics when I saw the link. I didn’t know we had a page on explicit mathematics, so I thought I’d take a look. :)
I can fill in some more details tomorrow, perhaps also with some references to PX, which used to be a proof assistant loosely based on explicit mathematics.
I’ve now added some more material and links to explicit mathematics.
Thanks! I don’t have time to read it now. But I just wanted to say, you don’t have to keep my very uninformative “related to constructive mathematics” as the first sentence. I wrote that only so that the page wouldn’t be totally uninformative about what explicit mathematics is, but I’m sure you can write a better first sentence.
1 to 5 of 5