Menu

Pragmas / Annotations

2013-11-13
2014-03-05
  • John Tang Boyland

    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.

     
  • John Tang Boyland

    For example:
    @Reduces(t1 >= t3)
    @InductionOn(p1,p2)
    @HasNegation

     
  • John Tang Boyland

    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.

     
  • John Tang Boyland

    The @ syntax is appealing for parsing purposes, but doesn't fit the original style of SASyLF: trying to follow structured natural language wherever possible.

     

Log in to post a comment.