intros.elim H1.assumption.
qed.
+default \"equality\"
+ " ^ buri ^ "/eq.ind
+ " ^ buri ^ "/sym_eq.con
+ " ^ buri ^ "/trans_eq.con
+ " ^ buri ^ "/eq_ind.con
+ " ^ buri ^ "/eq_elim_r.con
+ " ^ buri ^ "/eq_f.con
+ " ^ buri ^ "/eq_f1.con.
+
theorem eq_f: \\forall A,B:Type.\\forall f:A\\to B.
\\forall x,y:A. eq A x y \\to eq B (f x) (f y).
intros.elim H.reflexivity.
intros.elim H.reflexivity.
qed.
-default \"equality\"
- " ^ buri ^ "/eq.ind
- " ^ buri ^ "/sym_eq.con
- " ^ buri ^ "/trans_eq.con
- " ^ buri ^ "/eq_ind.con
- " ^ buri ^ "/eq_elim_r.con
- " ^ buri ^ "/eq_f.con
- " ^ buri ^ "/eq_f1.con.
-
inductive ex (A:Type) (P:A \\to Prop) : Prop \\def
ex_intro: \\forall x:A. P x \\to ex A P.
interpretation \"exists\" 'exists \\eta.x =
"
;;
-let p_to_ma ~tptppath ~filename =
+let p_to_ma ?timeout ~tptppath ~filename () =
let data =
- Tptp2grafite.tptp2grafite ~filename ~tptppath:tptppath
+ Tptp2grafite.tptp2grafite ?timeout ~filename ~tptppath:tptppath
~raw_preamble ()
in
data
;;
let main () =
- MatitaInit.fill_registry ();
let tptppath = ref "./" in
+ let timeout = ref 600 in
MatitaInit.add_cmdline_spec
["-tptppath",Arg.String (fun s -> tptppath:= s),
- "Where to find the Axioms/ and Problems/ directory"];
- MatitaInit.parse_cmdline ();
- MatitaInit.load_configuration_file ();
- Helm_registry.set_bool "db.nodb" true;
+ "Where to find the Axioms/ and Problems/ directory";
+ "-timeout", Arg.Int (fun x -> timeout := x),
+ "Timeout in seconds"];
+ MatitaInit.parse_cmdline_and_configuration_file ();
Helm_registry.set_bool "matita.nodisk" true;
HLog.set_log_callback (fun _ _ -> ());
let args = Helm_registry.get_list Helm_registry.string "matita.args" in
| [file] -> file
| _ -> prerr_endline "You must specify exactly one .p file."; exit 1
in
- let data = p_to_ma ~filename:inputfile ~tptppath:!tptppath in
+ let data =
+ p_to_ma ~timeout:!timeout ~filename:inputfile ~tptppath:!tptppath ()
+ in
(* prerr_endline data; *)
let is = Ulexing.from_utf8_string data in
let gs = GrafiteSync.init () in