GrafiteAst.Symmetry loc
| IDENT "transitivity"; t = tactic_term ->
GrafiteAst.Transitivity (loc, t)
+ (* Produzioni Aggiunte *)
+ | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
+ GrafiteAst.Assume (loc, id, t)
+ | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
+ GrafiteAst.Suppose (loc, t, id)
+ | IDENT "by" ; t = tactic_term ; IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
+ GrafiteAst.By_term_we_proved (loc, t, ty, id)
+ | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
+ GrafiteAst.We_need_to_prove (loc, t, id)
+ | IDENT "by" ; t = tactic_term ; IDENT "done" ->
+ GrafiteAst.Bydone (loc, t)
]
];
atomic_tactical:
] ];
macro: [
- [ [ IDENT "quit" ] -> GrafiteAst.Quit loc
-(* | [ IDENT "abort" ] -> GrafiteAst.Abort loc *)
-(* | [ IDENT "undo" ]; steps = OPT NUMBER ->
- GrafiteAst.Undo (loc, int_opt steps)
- | [ IDENT "redo" ]; steps = OPT NUMBER ->
- GrafiteAst.Redo (loc, int_opt steps) *)
- | [ IDENT "check" ]; t = term ->
+ [ [ IDENT "check" ]; t = term ->
GrafiteAst.Check (loc, t)
| [ IDENT "hint" ] -> GrafiteAst.Hint loc
| [ IDENT "whelp"; "match" ] ; t = term ->
GrafiteAst.WElim (loc, t)
| [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
GrafiteAst.WHint (loc,t)
- | [ IDENT "print" ]; name = QSTRING -> GrafiteAst.Print (loc, name)
]
];
alias_spec: [