let pnv,piv= (fun expr -> string_of_lambda (cbv expr)), (fun expr -> to_int (cbv expr))
let db, db_equal, db_contains = db, db_equal, db_contains
+let alpha_eq x f = db_equal (db x) (db y)
+
(* or *)
let add = << fun m n -> fun s z -> m s (n s z) >>;;
- church_to_int << $add$ $one$ $two$ >>;;
+ (* now use:
+ pp FORMULA to print a formula, unreduced
+ pn FORMULA to print the normal form of a formula (when possible)
+ pi FORMULA to print the integer which FORMULA is a Church numeral for (when possible)
+
+ alpha_eq FORM1 FORM2 are FORM1 and FORM2 syntactically equivalent (up to alpha-conversion)?
+ this does not do reductions on the formulae
+ *)
+
+ pi << $add$ $one$ $two$ >>;;
- : int = 3
To install this package, here's what you need to do. I've tried to explain it in basic terms, but you do need some familiarity with your operating system: for instance, how to open a Terminal window, how to figure out what directory the Terminal is open to (use `pwd`); how to change directories (use `cd`); and so on.