Skip to content
GitLab
Explore
Sign in
Rice Wine
Iris
Repository
iris
tests
proofmode.v
Find file
Blame
History
Permalink
Validity coercion from iProp to Prop. Magic wand that works at the Prop level.
· 243fdd13
Jacques-Henri Jourdan
authored
Nov 24, 2016
The idea on magic wand is to use it for curried lemmas and use ⊢ for uncurried lemmas.
243fdd13