]
] in
let ens = [
- (UriManager.uri_of_string"cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var",
+ (UriManager.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var",
C.Rel 4);
- (UriManager.uri_of_string"cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var",
+ (UriManager.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var",
C.Rel 3);
- (UriManager.uri_of_string"cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var",
+ (UriManager.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var",
C.Rel 2);
] in
let term2 = C.Appl [
Printf.printf "OK, %s ha tipo %s\n" (CicPp.ppterm term2) (CicPp.ppterm ty);
;;
+
+let test_lib () =
+ let uri = Sys.argv.(1) in
+ let t = CicUtil.term_of_uri (UriManager.uri_of_string uri) in
+ let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
+ Printf.printf "Term of %s: %s\n" uri (CicPp.ppterm t);
+ Printf.printf "type: %s\n" (CicPp.ppterm ty);
+;;
+
+
(* differing ();; *)
(* next_after ();; *)
(* discrimination_tree_test ();; *)
(* path_indexing_test ();; *)
(* test_subst ();; *)
Helm_registry.load_from "../../matita/matita.conf.xml";
-test_refl ();;
+(* test_refl ();; *)
+test_lib ();;