entrypoints Prog, Expr;

layout toplevel ;

token VarName letter (lower | upper | digit)* ;

Prog. Prog ::= [Decl] ;

separator Decl ";" ;

Def.   Decl ::= VarName ":" Expr "=" Expr ;
Axiom. Decl ::= VarName ":" Expr ;

Lam.  Expr  ::= "\\" [VarName] "->" Expr ;
Pi.   Expr  ::= [Binding] "->" Expr ;
Fun.  Expr  ::= Expr1 "->" Expr ;
_.    Expr  ::= Expr1;
Apps. Expr1 ::= [Expr2] ;
Var.  Expr2 ::= VarName ;
Star. Expr2 ::= "*";
_.    Expr2 ::= "(" Expr ")";

Bind. Binding ::= "(" [Expr2] ":" Expr ")" ;
separator nonempty Binding "" ;

separator nonempty Expr2 "" ;
separator nonempty VarName "" ;

comment "--" ;