tests/proofmode.v · 6e334252ef3e6162bfccd2cd3879b8c78b431a1d · Yixuan Chen / Iris · GitLab

Snippets Groups Projects

Forked from Iris / Iris

Source project has a limited visibility.

4 years ago
6e334252
Remove property `(∀ a, ⌜ φ a ⌝) ⊢ ⌜ ∀ a, φ a ⌝` from the BI canonical structure and · 6e334252
Robbert Krebbers authored 4 years ago
```
put it into a type class `BiPureForall`.

This property does not hold for embeddings of classical logic into Coq.
```
6e334252

History
Remove property `(∀ a, ⌜ φ a ⌝) ⊢ ⌜ ∀ a, φ a ⌝` from the BI canonical structure and
Robbert Krebbers authored 4 years ago
```
put it into a type class `BiPureForall`.

This property does not hold for embeddings of classical logic into Coq.
```