From 72c158e8d807d2ca59fde96b2f06f0dbb8055ba9 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Mon, 20 Sep 2010 12:16:44 -0400 Subject: [PATCH] tweak ml code/instructions Signed-off-by: Jim Pryor --- code/lambda.ml | 2 ++ using_the_programming_languages.mdwn | 11 ++++++++++- 2 files changed, 12 insertions(+), 1 deletion(-) 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. -- 2.11.0