gistfile1.txt

grammar Var x y z == String.

grammar Term M N P ::=
  var x,  x, "variable";
  zero, "zero", "zero";
  suc M, "suc" M, "successor";
  pair M N , "<" M "," N ">" , "pair";
  fst P , "fst" P , "fst";
  snd P , "snd" P , "snd";
  lam x M, "\\" x "->" M, "lambda";
  app M N, M N, "application".

grammar Type A B C ::=
  nat, "Nat", "number";
  prod A B, A "*" B, "product";
  fun A B, A "->" B, "function".

grammar TypeDecl J ::=
  has-type x A, x ":" A, "variable".

grammar Context \Gamma ::=
  nil, "[]", "empty context";
  snoc \Gamma J, \Gamma "," J, "non-empty context".

judgment Hyp \Gamma J, \Gamma "\ni" J where
  here : Hyp (snoc \Gamma) J;
  there : Hyp \Gamma (has-type x A) -> x != y -> Hyp (snoc \Gamma (has-type y B)) (has-type x A).

judgment HasType \Gamma M A where
  var-type : Hyp \Gamma (has-type x A) -> HasType \Gamma (var x) A;
  zero-type : HasType \Gamma zero nat;
  suc-type : HasType \Gamma M nat -> HasType \Gamma (suc M) nat;
  pair-type : HasType \Gamma M A -> HasType \Gamma N A -> HasType \Gamma (pair M N) (prod A B);
  fst-type : HasType \Gamma P (prod A B) -> HasType \Gamma (fst P) A;
  snd-type : HasType \Gamma P (prod A B) -> HasType \Gamma (snd P) B;
  lam-type : HasType (snoc \Gamma (has-type x A)) M B -> HasType \Gamma (lam x M) (fun A B);
  app-type : HasType \Gamma M (fun A B) -> HasType \Gamma N A -> HasType \Gamma (app M N) B.