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 2
TVar.   Term2 ::= Id;

TType.  Term2 ::= "Type";

TT0.    Term2 ::= "𝟘";

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

TBool.  Term2 ::= "𝟚";
TTrue.  Term2 ::= "true";
TFalse. Term2 ::= "false";

TNat.   Term2 ::= "ℕ";
TZero.  Term2 ::= "0";

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

-- Term1
TInd0.  Term1 ::= "𝟘-elim" Term2 Term2;

TIndB.  Term1 ::= "𝟚-elim" Term2 Term2 Term2 Term2;

TSuc.   Term1 ::= "suc" Term2;
TIndN.  Term1 ::= "ℕ-elim" Term2 Term2 Term2 Term2;

TFst.   Term1 ::= "pr₁" Term2;
TSnd.   Term1 ::= "pr₂" Term2;

TApp.   Term1 ::= Term1 Term2;

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

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

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


coercions Term 2;