lambda_calc_notations.v

Require Import Coq.Strings.String. Open Scope string_scope.

Inductive expr :=
| EVar(x: string)
| ELam(x: string)(body: expr)
| EApp(f: expr)(arg: expr).

Declare Custom Entry ident_string.
Notation "x" := x (in custom ident_string at level 0, x constr at level 0).

Declare Custom Entry lambda_expr.

Notation "x" := (EVar x)
  (in custom lambda_expr at level 0, x custom ident_string).

Notation "'expr:(' x )" := x
   (x custom lambda_expr at level 100, format "expr:( x )").

Notation "( x )" := x
  (in custom lambda_expr at level 0, x custom lambda_expr at level 100).

Notation "'coq:(' x )" := x
  (in custom lambda_expr at level 0, x constr at level 200,
   format "'coq:(' x )").

Notation "f x" := (EApp f x)
  (in custom lambda_expr at level 10, left associativity,
   format "'[  ' f  x ']'").

Notation "'fun' x => body" := (ELam x body)
  (in custom lambda_expr at level 100, x custom ident_string,
   body custom lambda_expr at level 100,
   format "'[  ' 'fun'  x  =>  '/' body ']'").
Notation "'fun' x y .. z => body" := (ELam x (ELam y .. (ELam z body) ..))
  (in custom lambda_expr at level 100,
   x custom ident_string, y custom ident_string, z custom ident_string,
   body custom lambda_expr at level 100,
   format "'[  ' 'fun'  x  y  ..  z  =>  '/' body ']'").

Notation "'let' x := rhs 'in' body" := (EApp (ELam x body) rhs)
  (in custom lambda_expr at level 100, x custom ident_string, right associativity,
   format "'[' 'let'  x  :=  '[' rhs ']'  'in'  '/' body ']'").

Example ChurchNumerals := expr:(
  let "zero" := fun "f" "x" => "x" in
  let "succ" := fun "m" "f" "x" => "m" "f" ("f" "x") in
  let "plus" := fun "m" "n" "f" "x" => "m" "f" ("n" "f" "x") in
  let "one" := "succ" "zero" in
  let "two" := "succ" "one" in
  "plus" "two" "two"
).

Print ChurchNumerals.
(* prints
ChurchNumerals =
expr:(let "zero" := fun "f" "x" => "x" in
      let "succ" := fun "m" "f" "x" => "m" "f" ("f" "x") in
      let "plus" := fun "m" "n" "f" "x" => "m" "f" ("n" "f" "x") in
      let "one" := "succ" "zero" in let "two" := "succ" "one" in "plus" "two" "two")
     : expr
*)