Skip to content

make the proof term in the readiness type class "unreferencable"

Björn Brandenburg requested to merge dont-name-readiness-proof-term into master

As discussed at the RT-PROOFS meeting in Paris, proof terms should not have a name so that we don't actually directly depend on them in proofs. This patch removes the explicit name of the proof term in the readiness type class and introduces an equivalent lemma.

CC: @sbozhko and @mlesourd, please check that this matches what we agreed on.

Merge request reports