| IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
let uris = List.map UriManager.uri_of_string uris in
GrafiteAst.Default (loc,what,uris)
+ | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
+ refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
+ refl = tactic_term -> refl ] ;
+ sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
+ sym = tactic_term -> sym ] ;
+ trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
+ trans = tactic_term -> trans ] ;
+ "as" ; id = IDENT ->
+ GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
]];
lexicon_command: [ [
IDENT "alias" ; spec = alias_spec ->