Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
  • robbert/cmra_valid_elim
  • ralf/separable
  • robbert/mono_Z
  • ralf/Z
  • ralf/bi-persistently-emp
  • ralf/mono_Z
  • ci/robbert/big_op_binder
  • robbert/no_native_compute
  • simon/parametric-index
  • ci/robbert/set_solver_eauto
  • ralf/make
  • ci/msammler/nb_state
  • robbert/add_sub
  • ci/general-contractive
  • ralf/has-lc
  • robbert/has_lc_if
  • robbert/bi_cofe
  • robbert/bi_wand_notation
  • robbert/level
20 results
An error occurred while fetching tags. Retry the search.
Compare
Forked from Iris / Iris
5710 commits behind the upstream repository.
user avatar
Validity coercion from iProp to Prop. Magic wand that works at the Prop level.
Jacques-Henri Jourdan authored 
    The idea on magic wand is to use it for curried lemmas and use ⊢ for uncurried lemmas.
243fdd13
History
user avatar 243fdd13
History