Skip to content

docs: fix bug in ghost resource laws

Jeehoon Kang requested to merge jeehoon.kang/iris-coq:master into master

I think the current rule if buggy; the validity of a ghost resource a should not imply its ownership.

Please advise me if I understand incorrectly :-) Thank you! Jeehoon

Merge request reports