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;
ExpAppI.   Exp1 ::= Exp1 "{" Exp "}";
ExpAppE.   Exp1 ::= Exp1 Exp2;
ExpFst.    Exp1 ::= "pr₁" Exp2;
ExpSnd.    Exp1 ::= "pr₂" Exp2;
ExpSuc.    Exp1 ::= "S" Exp2;

ExpInd0.   Exp1 ::= "⊥-elim" "⟦" Id "⇒" Exp "⟧" Exp2;
ExpIndN.   Exp1 ::= "ℕ-elim" "⟦" Id        "⇒" Exp "⟧"
                             "⟦" "0"       "⇒" Exp
			     "," "S" Id Id "⇒" Exp "⟧" Exp2;
ExpIndB.   Exp1 ::= "𝔹-elim" "⟦" Id  "⇒" Exp "⟧"
                             "⟦" "T" "⇒" Exp
			     "," "F" "⇒" Exp "⟧" Exp2;

ExpVar.    Exp2 ::= Id;
ExpT0.     Exp2 ::= "⊥";
ExpT1.     Exp2 ::= "⊤";
ExpT1tr.   Exp2 ::= "⋆";
ExpTNat.   Exp2 ::= "ℕ";
ExpZero.   Exp2 ::= "0";
ExpTBool.  Exp2 ::= "𝔹";
ExpTrue.   Exp2 ::= "T";
ExpFalse.  Exp2 ::= "F";
ExpPair.   Exp2 ::= "⟨" Exp "," Exp "⟩";
ExpHole.   Exp2 ::= "?";


coercions Exp 2 ;

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

separator Def "" ;