Dead link in the README; question on examples of use

[herbelin]

Hi, the link https://www.pédrot.fr/articles/draft-forcing.pdf in the readme fails. Should it be e.g. https://www.pédrot.fr/articles/lics2016.pdf ?

Incidentally, do you have a list of examples of proofs done with the plugin. I'm thinking in particular to possible adaptations of standard set-theoretic proofs to type theory (when those proofs are constructive)?

[ppedrot]

Should it be e.g. https://www.pédrot.fr/articles/lics2016.pdf ?

I believe so.

Incidentally, do you have a list of examples of proofs done with the plugin.

Nothing involved, I am afraid. IIRC the most we tried to do were fixpoints with the later modality. What kind of standard proofs were you thinking about?

[herbelin]

Nothing involved, I am afraid. IIRC the most we tried to do were fixpoints with the later modality. What kind of standard proofs were you thinking about?

I had in mind a constructive adaptation of the proof of the negation of the continuum hypothesis to type theory, but also a forcing-based proof of Tarski completeness of my own vintage. As far as I understand, the Forcing Translate command of the plugin would allow to do that relatively easily without having to prove every sublemma in forcing style.