issues
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
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Update README.md
#18
radeusgd
opened
3 years ago
0
Inductive predicates vs Fixpoints
#17
radeusgd
opened
4 years ago
0
Multiple binders in patterns
#16
radeusgd
closed
4 years ago
3
Ids instance for explicitly typed terms
#15
radeusgd
closed
4 years ago
5
Extend STLC with explicit type annotations
#14
radeusgd
closed
4 years ago
1
Add fix operator
#13
radeusgd
closed
4 years ago
1
Add pattern matching
#12
radeusgd
opened
4 years ago
2
Add quotes and splices
#11
radeusgd
closed
4 years ago
2
Extend STLC with a boxed type and lift
#10
radeusgd
closed
4 years ago
0
STLC with autosubst
#9
radeusgd
closed
4 years ago
0
Quickly applying a hypothesis with a quantifier.
#8
radeusgd
closed
4 years ago
1
Order of quantifiers in theorems proven by induction
#7
radeusgd
closed
4 years ago
0
Handling names / binders
#6
radeusgd
closed
4 years ago
14
Case analysis of equality
#5
radeusgd
closed
4 years ago
3
Hints for tactics
#4
radeusgd
opened
4 years ago
2
Notation
#3
radeusgd
closed
4 years ago
0
Induction over mutually recursive types
#2
radeusgd
closed
4 years ago
6
Non-trivially recursive functions termination
#1
radeusgd
closed
4 years ago
1