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