In order to make extensions easier and more parser friendly, we would like to add the ability to add Java-style @annotations to syntax, judgments and theorems. "assumes" would be retrofitted as such an annotation.
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
Actually "assumes" has a strong semantic meaning and should not be replaced with a pragma. A judgment that uses a context without assumes cannot do binding, for example.
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
The @ syntax is appealing for parsing purposes, but doesn't fit the original style of SASyLF: trying to follow structured natural language wherever possible.
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
In order to make extensions easier and more parser friendly, we would like to add the ability to add Java-style @annotations to syntax, judgments and theorems. "assumes" would be retrofitted as such an annotation.
For example:
@Reduces(t1 >= t3)
@InductionOn(p1,p2)
@HasNegation
Actually "assumes" has a strong semantic meaning and should not be replaced with a pragma. A judgment that uses a context without assumes cannot do binding, for example.
The
@
syntax is appealing for parsing purposes, but doesn't fit the original style of SASyLF: trying to follow structured natural language wherever possible.