base_logic/double_negation.v · f2bf449c3ee8cea0d02106565a999193bf961bdc · William Mansky / Iris · GitLab

Snippets Groups Projects

Forked from Iris / Iris

5219 commits behind the upstream repository.

8 years ago
243fdd13
Validity coercion from iProp to Prop. Magic wand that works at the Prop level. · 243fdd13
Jacques-Henri Jourdan authored 8 years ago
```
    The idea on magic wand is to use it for curried lemmas and use ⊢ for uncurried lemmas.
```
243fdd13

History
Validity coercion from iProp to Prop. Magic wand that works at the Prop level.
Jacques-Henri Jourdan authored 8 years ago
```
    The idea on magic wand is to use it for curried lemmas and use ⊢ for uncurried lemmas.
```