entrypoints [Def], Term;

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

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

Defn. Def ::= "def" Id ":" Term ":=" Term;
separator nonempty Def "" ;

-- names bound by lambdas
NImp.   Name ::= "{" Id "}";
NExp.   Name ::= Id;
separator nonempty Name "" ;

-- Term 3
TType.  Term3 ::= "Type";

TT0.    Term3 ::= "𝟘";
TInd0.  Term3 ::= "𝟘-elim";

TT1.    Term3 ::= "𝟙";
TT1tr.  Term3 ::= "★";

TBool.  Term3 ::= "𝟚";
TTrue.  Term3 ::= "true";
TFalse. Term3 ::= "false";
TIndB.  Term3 ::= "𝟚-elim";

TNat.   Term3 ::= "ℕ";
TZero.  Term3 ::= "0";
TSuc.   Term3 ::= "suc";
TIndN.  Term3 ::= "ℕ-elim";

TFst.   Term3 ::= "pr₁";
TSnd.   Term3 ::= "pr₂";

TLam.   Term3 ::= "λ" [Name] "." Term;

TVar.   Term3 ::= Id;

-- Term2

TAppEx. Term2 ::= Term2 Term3;
TAppIm. Term2 ::= Term2 "{" Term "}";

-- Term1
TPiAr.  Term1 ::= Term2 "→" Term1;
TSgCr.  Term1 ::= Term2 "×" Term1;

-- Term0
TLet.   Term ::= "let" Id ":" Term ":=" Term "in" Term ;

TPiEx.  Term ::= "(" Id ":" Term ")" "→" Term;
TPiIm.  Term ::= "{" Id ":" Term "}" "→" Term;

TSg.    Term ::= "(" Id ":" Term ")" "×" Term;
TPair.  Term ::= "⟨" Term "," Term "⟩";

THole.  Term ::= "?";

coercions Term 3;