Skip to content
GitLab
Explore
Sign in
Simon Spies
Iris
Repository
iris
proofmode
intro_patterns.v
Find file
Blame
History
Permalink
Enable $-prefixes in ssr-like {H1 .. Hn} intro-patterns to perform framing.
· a9f8d0f0
Robbert Krebbers
authored
Jun 30, 2016
For example iIntros "{$H1 H2} H1" frames H1, clears H2, and introduces H1.
a9f8d0f0