Skip to content

Plainly

Daniël Louwrink requested to merge daniel/plainly into master

This merge requests changes the typing, subtyping, environment splitting and environment copying judgments to be Plain, by wrapping them in a plainly modality. Furthermore, it fixes the proofs the typing rules for copy- and adds some missing rules.

This is based on the copying branch, hence that branch should probably be merged first.

Merge request reports