Merge branch 'robbert/fixpoint' into 'master'
Strengthen `bi_mono_pred` to ensure that functions are non-expansive. See merge request iris/iris!718
No related branches found
No related tags found
Showing
- CHANGELOG.md 3 additions, 1 deletionCHANGELOG.md
- iris/bi/lib/atomic.v 1 addition, 1 deletioniris/bi/lib/atomic.v
- iris/bi/lib/fixpoint.v 8 additions, 4 deletionsiris/bi/lib/fixpoint.v
- iris/bi/lib/relations.v 1 addition, 1 deletioniris/bi/lib/relations.v
- iris/program_logic/total_adequacy.v 1 addition, 1 deletioniris/program_logic/total_adequacy.v
- iris/program_logic/total_weakestpre.v 1 addition, 1 deletioniris/program_logic/total_weakestpre.v
Loading
Please register or sign in to comment