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.028Sep272120191514131298765432131Aug302928272625242322212019181716141110986542128Jul272625232221201918161513121165432130Jun2827262524232120191817161514876131May302928272524232221201913121110976Introduce 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.Mononicity of own.Lemma for inclusion of excl similar to dec_agree.Setoid injectivity of Some.Lemma for inclusion of dec_agree.Lemma for inclusion of singleton gmaps.Validity lemmas for deletion in gmaps.Destructors for csum.Make it possible to frame hypotheses using specialization patterns.Make iFrame finish the goal if everything has been framed.Better representation of specialization patterns.Validity and update lemmas for owning multiple ghosts.Use ⊆ type class for set-like inclusion of lists.Make iSplit{L,R} ignore persistent hypotheses.Define shorthand EqDecision A := (∀ x y : A, Decision (x = y)).