phlegmaticprogrammer
commented
9 years ago In addition to quotations of the form ‹ ... › there are now quotations of the form « ... ». In term or type literals they have identical meaning. In term or type patterns though, quotations of the form « ... » preserve their original meaning, i.e. they are used to dynamically insert terms and types into the pattern.
Quotations in patterns are usually interpreted as holes which contain patterns. But there are also use cases where quotations in patterns serve the same purpose as quotations in expressions, namely to insert other expressions dynamically. We want these kinds of quotations in patterns as well. See https://groups.google.com/forum/#!topic/proofpeer-dev/L4i9HGvi3No for some context.