Skip to content

Done, auto frame, and persistent frame specialization patterns

Robbert Krebbers requested to merge more_spec_patterns into master

This MR fixes issue #73 (closed): the // specialization pattern, the auto frame pattern [$], and enables framing in [#].

A note: I changed the syntax of the specialization pattern >[H1 .. Hn] into [> H1 .. Hn], which is much more consistent with [# H1 .. Hn] and [%]. This will break backwards compatibility, but the >[H1 .. Hn] patterns are not used often, so this should be easy to fix.

Merge request reports