::= [a-zA-Z0-9_!?] [a-zA-Z0-9_!?']* | '{|' '|}' ::= [a-zA-Z0-9_]* | '{|' '|}' ::= '.' ::= 'injective' | 'private' | 'private' 'injective' | 'def' ::= [x+] ::= + '.' | 'def' )> [] ':=' '.' | 'thm' )> ':' ':=' '.' | [] )> '.' | 'def'AC '[' ']' '.' | 'private' 'def'AC '[' ']' '.' | 'def'ACU '[' ',' ']' '.' | 'private' 'def'ACU '[' ',' ']' '.' | '#EVAL' '.' | '#EVAL' '.' | '#INFER' '.' | '#INFER' '.' | '#CHECK' ':' '.' | '#CHECKNOT' ':' '.' | '#ASSERT' ':' '.' | '#ASSERTNOT' ':' '.' | '#CHECK' '=' '.' | '#CHECKNOT' '=' '.' | '#ASSERT' '=' '.' | '#ASSERTNOT' '=' '.' | '#PRINT' '"' '"' '.' | '#GDT' '.' | '#GDT' '.' | '#NAME' '.' | '#REQUIRE' '.' | PRAGMA | EOF ::= '[' (',' )* ']' ::= ':' ::= '(' ':' ')' ::= '[' ']' '-->' | '{' '}' '[' ']' '-->' | '{' '}' '[' ']' '-->' ::= ':' | ::= [ (',' )*] ::= * | * | '(' ')' * ::= ::= | | '{' '}' | '(' ')' ::= '=>' | + ::= | | '(' ')' | 'Type' ::= * ::= | ':' '->' | '(' ':' ')' '->' | '->' | '=>' | ':' '=>' | '(' ':' ':=' ')' '=>'