Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • ci/debug
  • ci/for_proph
  • ci/hai/siProp
  • ci/janno/strict-tc-resolution
  • ci/ralf/Z_of_nat
  • ci/ralf/bi-language
  • ci/ralf/frame-frac
  • ci/robbert/contractive_ne
  • ci/robbert/coq_bug_7773
  • ci/robbert/faster_iDestruct
  • ci/robbert/faster_iDestruct2
  • ci/robbert/faster_iFresh_joe
  • ci/robbert/frame_fractional
  • ci/robbert/iFrame
  • ci/robbert/into_fupd
  • ci/robbert/into_val_pures
  • ci/robbert/kill_locked_value_lambdas
  • ci/robbert/mapsto_persist
  • ci/robbert/merge_sbi
  • ci/robbert/naive_solver
  • iris-3.5.0
  • iris-3.4.0
  • iris-3.3.0
  • iris-3.2.0
  • iris-3.1.0
  • iris-3.0.0
  • iris-2.0
  • iris-2.0-rc2
  • iris-2.0-rc1
  • iris-1.1
  • iris-1.0
  • hope-2015-coq-1
  • appendix-1.0.0
  • appendix-1
34 results
Created with Raphaël 2.2.05Oct43228Sep272120191514131298765432131Aug302928272625242322212019181716141110986542128Jul272625232221201918161513121165432130Jun2827262524232120191817161514876131May30292827252423222120No longer put proof mode class instances in their own file.Get rid of IntoAssert class.Functor for function space cofes.Define FromOp type class and use it in the proof mode.Fix the lemma Some_included' for total CMRAs.tweak the Qp lemmasdocs: update modelappendix: base logic is now up-to-datestart updating the appendix to iris 3.0Add lemmas about Qp and fractionDefine acquire of spin lock in terms of try_acquire.Fix link in ProofMode.md.Links in ProofMode.md.More links in README.Try to use links in README.Non step-indexed laws about exclusive and Some.Alternative definition of is_Some.Prove that the auth fragment is a UCMRA homomorphism.Unfolding lemmas for big ops over lists with Z indices.Extensionality (for Leibniz equality) of big ops.Deallocation local updates for gset.Cancelation for union.Prove fact about exclusive and included.Big ops and None.Looking up into a gmap is a homomorphism.Prove that included on frac corresponds to the order on Qp.Leibniz equality variants of the commute lemmas for big ops.Introduce CMRA homomorphisms.Prove always_if_pure.Generic decider for emptyness of finite maps.Define big operators on uPred in terms of those on CMRAs.Proper instances for mononicity of CMRA op.Relate included on uPred to entails.Induction principle for finite sets with Leibniz equality.Remove uPred_big_and, it only use just complicates stuff.Generic properties for commuting big ops.Big ops over gmap without binder for the key.Reorganize big ops for CMRA based on those for uPred.Uniform syntax for selecting hypotheses.Put notations for proofmode environment manipulation into a module.