radeusgd / QuotedPatternMatchingProof

A mechanized proof of soundness of calculus defined in A Theory of Quoted Code Patterns which is a formalization of pattern matching on code available in Scala 3 as part of its new macro system.
3 stars 0 forks source link

Add quotes and splices #11

Closed radeusgd closed 4 years ago

radeusgd commented 4 years ago

Preservation is proved in 78fbbe0, Progress is a work in progress.

radeusgd commented 4 years ago

This was done in f04e11c27eb468df01d8b2df140597661225e3b2