constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
tactic_term: [ [ t = term LEVEL "90" -> t ] ];
ident_list1: [ [ LPAREN; idents = LIST1 IDENT; RPAREN -> idents ] ];
constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
tactic_term: [ [ t = term LEVEL "90" -> t ] ];
ident_list1: [ [ LPAREN; idents = LIST1 IDENT; RPAREN -> idents ] ];