search

jesper-bengtson / Charge

Higher-order separation logic framework in Coq
Other
1 stars 1 forks source link

Fix 'Pure' and the pure instances #3

Closed gmalecha closed 10 years ago

gmalecha commented 10 years ago

We need definitions of 'pure' that work well with all separation logics (classical and intuitionistic). The (current) <-> definition that I proposed originally doesn't work, as Jesper pointed out so we need to go back and change it and prove all of the relevant lemmas for /\, \/, ->, etc for all of the ways that we build BI logics.

I can volunteer to do this.

gmalecha commented 10 years ago

Fixed in commit: 713bf63a25ace5eafba5e6198fe8f37c6a046fbd