search

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

STLC with autosubst #9

Closed radeusgd closed 4 years ago

radeusgd commented 4 years ago

Finished in 6c330c02eaac0c0808ede7fddcb24bc0472fa744