proofmode/intro_patterns.v · 483e9a03ed8094b25e7a2975dd1071d1d44ce70b · Tej Chajed / iris · GitLab

Snippets Groups Projects

Forked from Iris / Iris

Source project has a limited visibility.

8 years ago
a9f8d0f0
Enable $-prefixes in ssr-like {H1 .. Hn} intro-patterns to perform framing. · a9f8d0f0
Robbert Krebbers authored 8 years ago
```
For example iIntros "{$H1 H2} H1" frames H1, clears H2, and introduces H1.
```
a9f8d0f0

History
Enable $-prefixes in ssr-like {H1 .. Hn} intro-patterns to perform framing.
Robbert Krebbers authored 8 years ago
```
For example iIntros "{$H1 H2} H1" frames H1, clears H2, and introduces H1.
```