ProofMode.md · c6af67f965f38c610131e67d81869f7ffe75b14a · Abel Nieto / Iris

Forked from Iris / Iris

Source project has a limited visibility.

6 years ago

Allow `iSpecialize` to be nested. · c6af67f9

It now supports the specialization pattern `(H spat1 .. spatn)`, which first
recursively specializes the hypothesis `H` using the specialization patterns
`spat1 .. spatn`.

c6af67f9

History

Allow `iSpecialize` to be nested.

Robbert Krebbers authored 6 years ago

It now supports the specialization pattern `(H spat1 .. spatn)`, which first
recursively specializes the hypothesis `H` using the specialization patterns
`spat1 .. spatn`.