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.027Oct134328Sep27212014929Aug24221917842127Jul25232220121153130Jun26231814131May30292723429Apr1311730Mar292322211110543227Feb2625242322212019171615141311109842127Jan222018161412422Dec2115118420Nov19181716113Feb110Jun5221May22Apr1615Mar225Feb2416138130Jan29272523Dec181623Nov1569Oct86230Sep251613126326Aug22976410Jul425Jun23171676524May22429Sep27Aug2115141224Jun1721May15121172Apr25Mar1424Feb221919Jan512Nov19Oct104Sep30Aug29242121Jun1411improve f_equiv docMake everything compile with Coq 8.6tweak the Qp lemmasAdd lemmas about Qp and fractionAlternative definition of is_Some.Cancelation for union.Generic decider for emptyness of finite maps.Induction principle for finite sets with Leibniz equality.Relate map_to_list to nil.Relate "elements" of a finite set to nil.Insert and singleton maps are non-empty.Setoid injectivity of Some.Use ⊆ 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.