type ast = VAR of String | LAM of String * ast | APP of ast * ast | CONST
of int | ADD of ast * ast
type val = BASIC of int | FUNCTION of val -> val | ...
Thanks, Matthias! I know this is way off topic, but I think it's the sort of
thing only Schemers understand, and I think HOL Light would be a lot better off
my problem got solved. There's a lot I didn't understand with your ML
explanation. Is this written down somewhere? How to write a ML interpreter in
ML using your type ideas? Are you saying I don't need camlp parsing? I would
find that hard to believe. Formal proofs in HOL Light are really just OCaml
programs where a lot of code has already been evaluated. Here's a simple
Hilbert geometry program in my dialect:
let ExistsPointOffLine = theorem `;
∀l. Line l ⇒ ∃Q. Q ∉ l
proof
intro_TAC ∀l, H1;
consider A B C such that
¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ ¬Collinear A B C [Distinct] by fol I3;
assume (A ∈ l) ∧ (B ∈ l) ∧ (C ∈ l) [all_on] by fol ∉;
Collinear A B C [] by fol H1 - Collinear_DEF;
fol - Distinct;
qed;
`;;
I think I need the `;[...]` construct, which at present just turns my proof
into a string without any backslash or newline problems, which is then passed
to my function theorem. The usual HOL Light style is like this, using instead
a function prove:
let MULT_0 = prove
(`!m. m * 0 = 0`,
INDUCT_TAC THEN ASM_REWRITE_TAC[MULT; ADD_CLAUSES]);;
Notice the related `[...]` construct, which I think sends the ordered pair off
to heavy camlp parsing.
Thanks for the 7th and 8th advice. I think my student is smart and
hard-working, and I (finally!) learned how to program reading your book HtDP,
so it sounds like you're saying that I should be able to teach it to my
student. I went to bootstrap-world.org and, uh, maybe I didn't look hard
enough, but I didn't find anything that looked juicy.
--
Best,
Bill
____________________
Racket Users list:
http://lists.racket-lang.org/users
