Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
1 result
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.021Mar2019161514131298765432128Feb27262524232221201918161514131298763231Jan2927252423222120191816131211107331Dec30292322212019181514131211108765432130Nov29282726242322212018161514verified compatibility with Coq 8.8 (CI coming later)bump std++; no changes neededStop iFrame from introducing modalitiesmove Frame instances to their own filesplit class_instances into BI and SBI instancedsplit derived_laws into BI and SBI lawsmove general BI things using the proofmode down into lib/Merge branch 'ralf/intuitionistically' into 'gen_proofmode'apply Robbert's feedbackFromAffinely instance for intuitionistic modalityteach framing about the intuitionistic modalityadd tons of instances for the intuitionistic modalityget rid of 2nd into_persistent_intuitionistically instanceMerge branch 'ralf/valid' into 'gen_proofmode'update iIntoEmpValid docsiIntoValid -> iIntoEmpValidrename valid -> emp_validrename affinely_persistently -> intuitionistically; and make it a TC-opaque definitionFix typo.Merge branch 'gen_proofmode' of https://gitlab.mpi-sws.org/FP/iris-coq into gen_proofmodeWeaken BI axiom `P ⊢ <pers> emp` into `emp ⊢ <pers> emp`.rename env_persistent -> env_intuitionisticmake the README less outdatedfix a fluketypono idea why I would think this implies monotonicity...pers-emp actually just needs `core ε = ε`Merge branch 'gen_proofmode' of https://gitlab.mpi-sws.org/FP/iris-coq into gen_proofmodeshow that persistently is also another fixpointMerge branch 'joe/fresh' into 'gen_proofmode'Reorganize monpred.v and no longer upclose bupd and fupd.iFresh: document the Ltac trick to force evaluation of the side-effect.note that forall_2 would be derivable in a classical meta-logicshow that persistently and affinely-persistently are fixpoints of somethingCoq future-compat: use qualified name foriFresh: Force start proof when iFresh is called.Store a counter in to assign fresh names with .Add hint for introducing absorbingly.Prove `<absorb> □ P ⊣⊢ <pers> P` and use it to refactor some stuff.also test wand