Skip to content
Snippets Groups Projects
Select Git revision
  • coq-stdpp-1.0
  • glen/finite-nodec
  • master default protected
  • msammler/bitvector
  • msammler/bool_decide_simpl_never
  • ralf/hint-mode-check
  • robbert/cbn
  • robbert/f_equiv_pointwise
  • robbert/from_option
  • robbert/map_filter_True_False
  • robbert/multiset_singleton
  • robbert/tc_opaque
  • tchajed/stdpp-sprop-gmap
  • coq-stdpp-1.6.0
  • coq-stdpp-1.5.0
  • coq-stdpp-1.4.0
  • coq-stdpp-1.3.0
  • coq-stdpp-1.2.1
  • coq-stdpp-1.2.0
  • coq-stdpp-1.1.0
  • coq-stdpp-1.0.0
21 results
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.020Sep14929Aug24221917842127Jul25232220121153130Jun26231814131May30292723429Apr1311730Mar292322211110543227Feb2625242322212019171615141311109842127Jan222018161412422Dec2115118420Nov19181716113Feb110Jun5221May22Apr1615Mar225Feb2416138130Jan29272523Dec181623Nov1569Oct86230Sep251613126326Aug22976410Jul425Jun23171676524May22429Sep27Aug2115141224Jun1721May15121172Apr25Mar1424Feb221919Jan512Nov19Oct104Sep30Aug29242121Jun1411Use ⊆ type class for set-like inclusion of lists.Define shorthand EqDecision A := (∀ x y : A, Decision (x = y)).Make Is_true a typeclass.Shorten proof of Qp_lower_bound a bit.Add lemma about the existence of a lower bound of two fractions.Make gmap_empty Opaque to avoid simpl unfolding it.Turn out Coq 8.5 already comes with a module to get lia without axioms: LiaBig ops over lists as binder.Now really get rid of the eq_rect_eq axiom.Prove UIP for decidable types without relying on the stdlib.use Psatz without using axioms about real numbersImport less Program stuff to avoid UIP/fun_ext showing up with coqchk.make coqchk happy with prelude.prettyMake coqchk slightly happier with prelude/prettyMerge branch 'master' of gitlab.mpi-sws.org:FP/iris-coqInhabited instance for any Empty instance.Better Coq 8.6 compatibilitySome general stuff about fin.Injectivity instance for Z.of_nat.Unfolding properties for Nat.iter.Sets of sequences of natural numbers.Conversion from coPset to gset positive.Make hlist universe polymorphic.Revert "Make the types of the finite map type classes more specific."Make the types of the finite map type classes more specific.Relate subseteq on collections to the extension order.More documentation of [coPset].Forgot to commit prelude/sorting, this fixes 6dbe0c27.Version of fresh using an existential.More mapset deciders.More coPset deciders.Move sorting stuff to separate file.Simplify collection spaghetti.Remove unused set_NoDup stuff.Improve organization of prelude/fin_collections.Remove some generic decision procedures for sets.More consistent file names for coPset, bset and set.Make ∖ left associative.Turn unused disjoint_union_difference into something more sensible.LeibnizEquiv instance for unit.