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.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