Skip to content
Snippets Groups Projects
Select Git revision
  • adamAndMath/mfail
  • janno/tc-opaque-unseal
  • master default protected
  • ralf/empty-opaque
  • ralf/listZ
  • ralf/hint-mode-plus
  • ci-release
  • robbert/set_fold_union
  • ci/msammler/more_feed
  • ci/msammler/_1_2_lemmas
  • dfrumin/coq-stdpp-set_map_2
  • robbert/set_guide
  • msammler/bitvector
  • msammler/bool_decide_simpl_never
  • robbert/map_filter_True_False
  • tchajed/stdpp-sprop-gmap
  • ralf/hint-mode-check
  • robbert/multiset_singleton
  • robbert/f_equiv_pointwise
  • robbert/cbn
  • coq-stdpp-1.8.0
  • coq-stdpp-1.7.0
  • 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
30 results
Compare
Forked from Iris / stdpp
Source project has a limited visibility.
user avatar
Prove "cross split" rule for Qp.
Robbert Krebbers authored 
Terminology taken from "A Fresh Look at Separation Algebras and Share"
by Dockins et al.
3bcaaf7e
History
user avatar 3bcaaf7e
History
Name Last commit Last update