+ sort: [
+ [ SYMBOL "\\PROP" -> ()
+ | SYMBOL "\\SET" -> ()
+ | SYMBOL "\\TYPE" -> ()
+ ]
+ ];
+ explicit_subst: [
+ [ (* TODO explicit substitution *)
+ ]
+ ];
+ meta_subst: [
+ [ (* TODO meta substitution *)
+ ]
+ ];
+ possibly_typed_name: [
+ [ SYMBOL "("; i = IDENT; SYMBOL ":"; typ = pattern; SYMBOL ")" -> ()
+ | i = IDENT -> ()
+ ]
+ ];
+ match_pattern: [
+ [ n = IDENT -> ()
+ | SYMBOL "("; head = IDENT; vars = LIST1 possibly_typed_name; SYMBOL ")" ->
+ ()
+ ]
+ ];
+ binder: [
+ [ SYMBOL <:unicode<Pi>> (* Π *) -> ()
+ | SYMBOL <:unicode<exists>> (* ∃ *) -> ()
+ | SYMBOL <:unicode<forall>> (* ∀ *) -> ()
+ | SYMBOL <:unicode<lambda>> (* λ *) -> ()
+ ]
+ ];
+ bound_names: [
+ [ vars = LIST1 IDENT SEP SYMBOL ",";
+ typ = OPT [ SYMBOL ":"; p = pattern -> () ] -> ()
+ | LIST1 [
+ SYMBOL "("; vars = LIST1 IDENT SEP SYMBOL ",";
+ typ = OPT [ SYMBOL ":"; p = pattern -> () ]; SYMBOL ")" -> ()
+ ] ->
+ ()
+ ]
+ ];
+ induction_kind: [
+ [ IDENT "rec" -> ()
+ | IDENT "corec" -> ()
+ ]
+ ];
+ let_defs: [
+ [ defs = LIST1 [
+ name = IDENT; args = bound_names;
+ index_name = OPT [ IDENT "on"; idx = IDENT -> () ];
+ ty = OPT [ SYMBOL ":" ; p = pattern -> () ];
+ SYMBOL <:unicode<def>> (* ≝ *); body = pattern ->
+ ()
+ ] SEP IDENT "and" ->
+ ()
+ ]
+ ];
+ pattern_variable: [
+ [ SYMBOL "\\NUM"; id = IDENT -> ()
+ | SYMBOL "\\IDENT"; id = IDENT -> ()
+ | SYMBOL "\\FRESH"; id = IDENT -> ()
+ ]
+ ];
+ magic_pattern: [
+ [ SYMBOL "\\FOLD"; n = OPT NUMBER; [ IDENT "left" | IDENT "right" ];
+ LIST1 IDENT; SYMBOL "."; p1 = pattern;
+ OPT [ SYMBOL "\\LAMBDA"; LIST1 IDENT ]; p2 = pattern ->
+ ()
+ | SYMBOL "\\DEFAULT"; id = IDENT; p1 = pattern; p2 = pattern -> ()
+ ]
+ ];
+ pattern:
+ [ "letin" NONA
+ [ IDENT "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
+ p1 = pattern; "in"; p2 = pattern ->
+ ()
+ | IDENT "let"; k = induction_kind; defs = let_defs; IDENT "in";
+ body = pattern ->
+ ()
+ ]
+ | "binder" RIGHTA
+ [ b = binder; bound_names; SYMBOL "."; body = pattern -> () ]
+ | "extension"
+ [ ]
+ | "apply" LEFTA
+ [ p1 = pattern; p2 = pattern -> () ]
+ | "simple" NONA
+ [ i = IDENT -> ()
+ | i = IDENT; s = explicit_subst -> ()
+ | n = NUMBER -> ()
+ | IMPLICIT -> ()
+ | m = META -> ()
+ | m = META; s = meta_subst -> ()
+ | s = sort -> ()
+ | s = SYMBOL -> ()
+ | u = URI -> ()
+ | outtyp = OPT [ SYMBOL "["; typ = pattern; SYMBOL "]" ];
+ IDENT "match"; t = pattern;
+ indty_ident = OPT [ SYMBOL ":"; id = IDENT ];
+ IDENT "with"; SYMBOL "[";
+ patterns = LIST0 [
+ lhs = match_pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *);
+ rhs = pattern ->
+ ()
+ ] SEP SYMBOL "|";
+ SYMBOL "]" ->
+ ()
+ | SYMBOL "("; p1 = pattern; SYMBOL ":"; p2 = pattern; SYMBOL ")" -> ()
+ | SYMBOL "("; p = pattern; SYMBOL ")" -> ()
+ | v = pattern_variable -> ()
+ | m = magic_pattern -> ()
+ ]
+ ];