1open HolKernel Parse boolLib bossLib;
2
3val _ = new_theory "github462";
4
5val _ = Datatype ���exp = Lit num | Log exp exp���;
6
7val _ = Datatype ���exp_or_val = Exp exp | Val num���;
8
9val do_log_def = Define ���do_log v e = ARB���;
10
11val eval_defn =
12Defn.Hol_defn
13 "eval"
14 ���(eval st [Log e1 e2] =
15    case eval st [e1] of
16        (st', SOME v1) => (case do_log (HD v1) e2 of
17                               SOME (Exp e) => eval st' [e]
18                             | SOME (Val v) => (st', SOME [v])
19                             | NONE => (st', NONE))
20      | res => res) /\
21  (eval st other = ARB)���;
22
23val _ = Defn.save_defn eval_defn
24
25fun test t =
26  not (can (find_term (same_const boolSyntax.select)) t)
27
28val _ = assert (List.all test o DefnBase.all_terms) eval_defn
29
30val _ = export_theory();
31