+(* {{{ Grammar for interpretation, notation level 3 *)
+GEXTEND Level3Parser
+ GLOBAL: level3_interpretation;
+ level3_interpretation: [ [ i = interpretation -> () ] ];
+ argument: [
+ [ i = IDENT -> ()
+ | SYMBOL <:unicode<eta>> (* η *); SYMBOL "."; a = SELF -> ()
+ | SYMBOL <:unicode<eta>> (* η *); i = IDENT; SYMBOL "."; a = SELF -> ()
+ ]
+ ];
+ term: [
+ [ u = URI -> ()
+ | a = argument -> ()
+ | SYMBOL "("; terms = LIST1 SELF; SYMBOL ")" -> ()
+ ]
+ ];
+ interpretation: [
+ [ IDENT "interpretation"; s = SYMBOL; args = LIST1 argument; IDENT "as";
+ t = term ->
+ ()
+ ]
+ ];
+END
+(* }}} *)
+