Skip to content
Snippets Groups Projects
Select Git revision
  • ascii-sections
  • basic-dune
  • bi_pure_scopes
  • doc-equalities
  • explicit-vdash
  • fix-497-hint-immediate
  • fix-notation
  • fupd-commutes
  • inv_exc_0_ipm
  • later-credits-drop
  • later_impl_experiments
  • later_impl_test
  • master default
  • more-convenient-fupd_proper
  • no-bi-canonical
  • notations
  • paolo/tc-strict-resolution-backport
  • periscopes
  • periscopes-v2
  • seal_ires
  • iris-4.3.0
  • iris-4.2.0
  • iris-4.1.0
  • 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
39 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.022Nov212019181716151098765432131Oct302827262522211817161514131210976543228Sep272120191514131298765432131Aug302928272625242322212019181716141110986542128Jul2726252322212019use OFEs instead of COFEs everywhereavoid leaving empty Makefile.coq if coq_makefile failsMerge branch 'master' of https://gitlab.mpi-sws.org/FP/iris-coqMakefile: make clean clean properlyComment on commit 44cfd7d3.Patch naive_solver to deal with Coq bug #2901.Function to convert a multiset into a gset.prove fmap_Some_setoidmake done and fast_done more consistent in behaviorMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqMore properties and set_solver for filter.Rename pure_equiv -> pure_True.simplify proof of step_fupd_mask_monoMove the defs of set_Forall and set_Exists out of the section.More generic definition of minimal that also for for anti-symmetric relations.Big op over set union.More type class opacity for multisets.Add some missing Proper instances on big ops.A generic filter operation on finite collections.Prove f <$> to_gmap x X = to_gmap (f x) X.Show that ⊆ on multisets is decidable.Prove to_gmap y (dom _ m) = const y <$> m.Write boxes lemmas with universally quantified mask.Remove unused parameters from some boxes lemmas.More big op lemmas.Support ■ (∀ _, _) and ■ (_ → _) in iIntros.Prove (■ φ → P) ⊣⊢ (∀ _ : φ, P).Minimal elements in a set.Multiset big ops on uPred.Homomorphism properties for big ops on multisets.More multiset properties.And also a variant when having to mapstos.Show that the fraction of a mapsto is valid.Also treat 009-013 as whitespace in the intro patterns parsers.Make own_valid_[n] and own_update_[n] curried.More big_opMS lemmas.Existentials commute with disjunction.Show that gmultiset is a simple collection.Add nclose N ⊆ E → nclose (N .@ x) ⊆ E to ndisj hints.Don't use Let outside of a section
Loading