Skip to content

Explicit vdash

Gregory Malecha requested to merge gmalecha/iris:explicit-vdash into master

This came as a result of the discussion in #270 (closed). It does a few things (unfortunately).

  • A new prefix |- P and |-@{PROP} P that ensures that P is parsed in I scope and acts like bi_emp_valid and sbi_emp_valid.
  • Removes the coercion status of bi_emp_valid and sbi_emp_valid
  • It moves notations that parse to types into type_scope since that scope is already set up appropriately.
  • It makes the -* at type_scope a parsing only notation.

People can decide what portions of this are good for merging.

Edited by Gregory Malecha

Merge request reports