entrypoints [Def], Exp ;

token Id ((letter|digit|["[]_"])+) ;

comment "--" ;
comment "{-" "-}" ;

BE. BD ::= Id;
BI. BD ::= "{" Id "}";
separator nonempty BD "" ;

ExpPiE.    Exp  ::= "Π" "(" Id ":" Exp ")" Exp;
ExpPiI.    Exp  ::= "Π" "{" Id ":" Exp "}" Exp;
ExpSig.    Exp  ::= "Σ" "(" Id ":" Exp ")" Exp;
ExpLet.    Exp  ::= "let" Id ":" Exp ":=" Exp "in" Exp;
ExpLam.    Exp  ::= "λ" [BD] "." Exp;
ExpApp.    Exp1 ::= Exp1 Exp2;
ExpVar.    Exp2 ::= Id;
ExpT0.     Exp2 ::= "⊥";
ExpT1.     Exp2 ::= "⊤";
ExpT1tr.   Exp2 ::= "⋆";
ExpTNat.   Exp2 ::= "ℕ";
ExpTZero.  Exp2 ::= "0";
ExpTSuc.   Exp2 ::= "S";
ExpTBool.  Exp2 ::= "𝔹";
ExpTTrue.  Exp2 ::= "T";
ExpTFalse. Exp2 ::= "F";
ExpTPair.  Exp2 ::= "⟨" Exp "," Exp "⟩";
ExpTFst.   Exp2 ::= "pr₁";
ExpTSnd.   Exp2 ::= "pr₂";

VarDef. Def ::= "def" Id ":" Exp ":=" Exp;

separator Def ";" ;