Showing
- iris/program_logic/ectxi_language.v 42 additions, 27 deletionsiris/program_logic/ectxi_language.v
- iris/program_logic/language.v 126 additions, 18 deletionsiris/program_logic/language.v
- iris/program_logic/lifting.v 68 additions, 41 deletionsiris/program_logic/lifting.v
- iris/program_logic/ownp.v 83 additions, 75 deletionsiris/program_logic/ownp.v
- iris/program_logic/total_adequacy.v 56 additions, 44 deletionsiris/program_logic/total_adequacy.v
- iris/program_logic/total_ectx_lifting.v 83 additions, 0 deletionsiris/program_logic/total_ectx_lifting.v
- iris/program_logic/total_lifting.v 16 additions, 16 deletionsiris/program_logic/total_lifting.v
- iris/program_logic/total_weakestpre.v 390 additions, 0 deletionsiris/program_logic/total_weakestpre.v
- iris/program_logic/weakestpre.v 505 additions, 0 deletionsiris/program_logic/weakestpre.v
- iris/proofmode/base.v 171 additions, 0 deletionsiris/proofmode/base.v
- iris/proofmode/class_instances.v 426 additions, 385 deletionsiris/proofmode/class_instances.v
- iris/proofmode/class_instances_embedding.v 221 additions, 0 deletionsiris/proofmode/class_instances_embedding.v
- iris/proofmode/class_instances_frame.v 477 additions, 0 deletionsiris/proofmode/class_instances_frame.v
- iris/proofmode/class_instances_internal_eq.v 68 additions, 0 deletionsiris/proofmode/class_instances_internal_eq.v
- iris/proofmode/class_instances_later.v 77 additions, 309 deletionsiris/proofmode/class_instances_later.v
- iris/proofmode/class_instances_make.v 190 additions, 0 deletionsiris/proofmode/class_instances_make.v
- iris/proofmode/class_instances_plainly.v 101 additions, 0 deletionsiris/proofmode/class_instances_plainly.v
- iris/proofmode/class_instances_updates.v 207 additions, 0 deletionsiris/proofmode/class_instances_updates.v
- iris/proofmode/classes.v 683 additions, 0 deletionsiris/proofmode/classes.v
- iris/proofmode/classes_make.v 149 additions, 0 deletionsiris/proofmode/classes_make.v
Some changes are not shown.
For a faster browsing experience, only 20 of 160+ files are shown.
iris/proofmode/class_instances_embedding.v
0 → 100644
iris/proofmode/class_instances_frame.v
0 → 100644
iris/proofmode/class_instances_internal_eq.v
0 → 100644
iris/proofmode/class_instances_make.v
0 → 100644
iris/proofmode/class_instances_plainly.v
0 → 100644
iris/proofmode/class_instances_updates.v
0 → 100644
iris/proofmode/classes_make.v
0 → 100644