From: Jim Pryor Date: Mon, 20 Sep 2010 16:16:44 +0000 (-0400) Subject: tweak ml code/instructions X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=72c158e8d807d2ca59fde96b2f06f0dbb8055ba9 tweak ml code/instructions Signed-off-by: Jim Pryor --- diff --git a/code/lambda.ml b/code/lambda.ml index 3f1435dc..146c9eb4 100644 --- a/code/lambda.ml +++ b/code/lambda.ml @@ -372,3 +372,5 @@ let pp, pn, pi = string_of_lambda, normal_string_of_lambda, int_of_lambda 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) + diff --git a/using_the_programming_languages.mdwn b/using_the_programming_languages.mdwn index deef2ee1..1fab79fa 100644 --- a/using_the_programming_languages.mdwn +++ b/using_the_programming_languages.mdwn @@ -44,7 +44,16 @@ know much OCaml yet to use it. Using it looks like this: (* 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.