Update core-spec for Coercion Quantification
ClosedPublic

Authored by ningning on Oct 20 2018, 7:56 AM.

Details

Summary

Update details for ForAllTy and ForAllCo in core-spec, as they
can now quantify over coercion variables.

Test Plan

Please read core-spec.pdf

ningning created this revision.Oct 20 2018, 7:56 AM
goldfire requested changes to this revision.Oct 21 2018, 8:51 PM
goldfire added inline comments.
docs/core-spec/Makefile
12

I think the original Makefile got this right: the mng file is the one with the [[ and ]] marks, which then produces a tex file. I double-checked in the ott manual about this, and the manual (IIUC) agrees with the original usage here.

docs/core-spec/core-spec.mng
225

Is that the right Note?

This revision now requires changes to proceed.Oct 21 2018, 8:51 PM
ningning added inline comments.Oct 21 2018, 9:39 PM
docs/core-spec/Makefile
12

Ok, I see. I will revert the renaming. My apologies.

docs/core-spec/core-spec.mng
225

Yes, it's "the last wrinkle..." in this note.
We have two notes with similar names, Note [unused coercion variable in ForAllTy] in TyCoRep, and Node [unused coercion variables in ForAllCo] in Coercion.

ningning updated this revision to Diff 18397.Oct 21 2018, 10:14 PM
ningning marked 2 inline comments as done.

revert renaming

goldfire accepted this revision.Oct 22 2018, 1:51 PM

Thanks!

This revision is now accepted and ready to land.Oct 22 2018, 1:51 PM
ningning edited the summary of this revision. (Show Details)Oct 22 2018, 9:48 PM
This revision was automatically updated to reflect the committed changes.