iris-lean icon indicating copy to clipboard operation
iris-lean copied to clipboard
verified publisher icon leanprover-community

Complete porting Plainly

Open ahuoguo opened this issue 1 month ago • 0 comments

https://github.com/leanprover-community/iris-lean/blob/master/src/Iris/BI/Plainly.lean is not fully done, which caused some issues in https://github.com/leanprover-community/iris-lean/pull/102

It will be nice to check if we ported the most relevant lemmas and instances of the derived connectives

ahuoguo avatar Dec 14 '25 00:12 ahuoguo