Skip to content
Snippets Groups Projects
Select Git revision
  • ci/debug
  • ci/for_proph
  • ci/general-contractive
  • ci/hai/siProp
  • ci/janno/strict-tc-resolution
  • ci/msammler/nb_state
  • ci/ralf/Z_of_nat
  • ci/ralf/bi-language
  • ci/robbert/big_op_binder
  • 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
  • iris-4.0.0
  • iris-3.6.0
  • 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
36 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.04Oct3228Sep272120191514131298765432131Aug302928272625242322212019181716141110986542128Jul272625232221201918161513121165432130Jun2827262524232120191817161514876131May302928272524232221201913121110More 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.Extend iClear to handle clearing of Coq-level variables.Use lazymatch in iClear to avoid backtracking on errors.Rename the internal validity uPred_valid into uPred_cmra_valid.Consistent syntax for generalization in iLöb and iInduction.CMRA structure on uPred.Relate map_to_list to nil.Relate "elements" of a finite set to nil.Alternative version of ownM_empty.Insert and singleton maps are non-empty.Binary mononicity property for CMRA op.Reorganize frame preserving updates for lists.More properties for the list CMRA.More derived auth properties.