<div dir="ltr">Dear Joe,<div><br></div><div>Is there any reason why you want to change some axioms in the files as "proofs"?</div><div>For example: </div><div><div><br></div><div>let ETA_AX =</div><div>  let axiom =</div><div>      let ty0 = mk_vartype "A" in</div><div>      let ty1 = mk_vartype "B" in</div><div>      let ty2 = mk_fun_ty ty0 ty1 in</div><div>      let ty3 = mk_type ("bool",[]) in</div><div>      let ty4 = mk_fun_ty ty2 ty3 in</div><div>      let tm0 = mk_var ("a",ty4) in</div><div>      let tm1 = mk_var ("b",ty2) in</div><div>      let tm2 = mk_var ("c",ty3) in</div><div>      let tm3 = mk_abs (tm2,tm2) in</div><div>      let tm4 = mk_eq (tm3,tm3) in</div><div>      let tm5 = mk_abs (tm1,tm4) in</div><div>      let tm6 = mk_eq (tm0,tm5) in</div><div>      let tm7 = mk_abs (tm0,tm6) in</div><div>      let tm8 = mk_var ("d",ty2) in</div><div>      let tm9 = mk_var ("e",ty0) in</div><div>      let tm10 = mk_comb (tm8,tm9) in</div><div>      let tm11 = mk_abs (tm9,tm10) in</div><div>      let tm12 = mk_eq (tm11,tm8) in</div><div>      let tm13 = mk_abs (tm8,tm12) in</div><div>      let tm14 = mk_comb (tm7,tm13) in</div><div>      new_axiom tm14</div><div>  in</div><div>  prove</div><div>    (`!(t:A->B). (\x. t x) = t`,</div><div>     PURE_REWRITE_TAC [FORALL_DEF; T_DEF] THEN</div><div>     ACCEPT_TAC axiom);;</div><div><br></div><div><br></div><div>instead of just :</div><div><br></div><div><div>let ETA_AX = new_axiom</div><div>  `!t:A->B. (\x. t x) = t`;;</div></div><div><br></div><div>Thanks!</div><div><br></div>-- <br><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><br></div><div>Regards,</div><div><a href="http://www.dptinfo.ens-cachan.fr/~swang/" target="_blank">Robert White </a>(Shuai Wang)</div><div><a href="https://www.rocq.inria.fr/deducteam/" target="_blank">INRIA Deducteam</a></div></div></div></div></div></div></div></div></div>
</div></div>