let _ = load_patterns21 []
+
+
val remove_notation: notation_id -> unit
(** {2 Notation enabling/disabling}
- * Right now, only disabling of notation during pretty printing is supporting.
+ * Right now, only disabling of notation during pretty printing is supported.
* If it is useful to disable it also for the input phase is still to be
* understood ... *)
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/legacy/coq/".
-
default "equality"
cic:/Coq/Init/Logic/eq.ind
cic:/Coq/Init/Logic/sym_eq.con
Z/dirichlet_product.ma Z/sigma_p.ma Z/times.ma nat/primes.ma
Z/moebius.ma Z/sigma_p.ma nat/factorization.ma
Z/times.ma Z/plus.ma nat/lt_arith.ma
-Z/orders.ma logic/connectives.ma Z/z.ma nat/orders.ma
+Z/orders.ma Z/z.ma logic/connectives.ma nat/orders.ma
Z/inversion.ma Z/dirichlet_product.ma Z/moebius.ma
Z/plus.ma Z/z.ma nat/minus.ma
Z/compare.ma Z/orders.ma nat/compare.ma
datatypes/constructors.ma logic/equality.ma
datatypes/compare.ma
datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma
-algebra/groups.ma logic/connectives.ma algebra/monoids.ma datatypes/bool.ma nat/compare.ma nat/le_arith.ma
-algebra/finite_groups.ma nat/relevant_equations.ma algebra/groups.ma
+algebra/groups.ma algebra/monoids.ma datatypes/bool.ma logic/connectives.ma nat/compare.ma nat/le_arith.ma
+algebra/finite_groups.ma algebra/groups.ma nat/relevant_equations.ma
algebra/semigroups.ma higher_order_defs/functions.ma
algebra/monoids.ma algebra/semigroups.ma
algebra/CoRN/SetoidInc.ma algebra/CoRN/SetoidFun.ma
algebra/CoRN/Setoids.ma Z/plus.ma datatypes/constructors.ma higher_order_defs/relations.ma logic/equality.ma nat/nat.ma
algebra/CoRN/SetoidFun.ma algebra/CoRN/Setoids.ma higher_order_defs/relations.ma
demo/propositional_sequent_calculus.ma datatypes/constructors.ma list/sort.ma nat/compare.ma nat/plus.ma
-demo/power_derivative.ma nat/nat.ma nat/compare.ma nat/orders.ma nat/plus.ma
+demo/power_derivative.ma nat/compare.ma nat/nat.ma nat/orders.ma nat/plus.ma
list/sort.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma
list/list.ma higher_order_defs/functions.ma logic/equality.ma nat/nat.ma
-logic/equality.ma logic/connectives.ma higher_order_defs/relations.ma
+logic/equality.ma higher_order_defs/relations.ma logic/connectives.ma
logic/connectives.ma
logic/coimplication.ma logic/connectives.ma
logic/connectives2.ma higher_order_defs/relations.ma
nat/nat.ma higher_order_defs/functions.ma
nat/relevant_equations.ma nat/gcd.ma nat/minus.ma nat/times.ma
nat/map_iter_p.ma nat/count.ma nat/permutation.ma
-nat/orders.ma logic/connectives.ma higher_order_defs/ordering.ma nat/nat.ma
+nat/orders.ma higher_order_defs/ordering.ma logic/connectives.ma nat/nat.ma
nat/pi_p.ma nat/generic_iter_p.ma nat/iteration2.ma nat/primes.ma
nat/plus.ma nat/nat.ma
nat/euler_theorem.ma nat/nat.ma nat/map_iter_p.ma nat/totient.ma
open GrafiteTypes
-exception AttemptToInsertAnAlias
+exception AttemptToInsertAnAlias of LexiconEngine.status
let out = ref ignore
let set_callback f = out := f
;;
let rec compile options fname =
- (* initialization, MOVE OUTSIDE *)
let matita_debug = Helm_registry.get_bool "matita.debug" in
- (* sanity checks *)
let include_paths = get_include_paths options in
let root,baseuri,fname,_tgt = Librarian.baseuri_of_script ~include_paths fname in
- let moo_fname =
- LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri ~writable:true
- in
- let lexicon_fname=
- LibraryMisc.lexicon_file_of_baseuri ~must_exist:false ~baseuri ~writable:true
- in
- if Http_getter_storage.is_read_only baseuri then
- HLog.error
- (Printf.sprintf "uri %s belongs to a read-only repository" baseuri);
- (* cleanup of previously compiled objects *)
- if (not (Http_getter_storage.is_empty ~local:true baseuri) ||
- LibraryClean.db_uris_of_baseuri baseuri <> [])
- then begin
- HLog.message ("baseuri " ^ baseuri ^ " is not empty");
- HLog.message ("cleaning baseuri " ^ baseuri);
- LibraryClean.clean_baseuris [baseuri];
- assert (Http_getter_storage.is_empty ~local:true baseuri);
- end;
- (* create dir for XML files *)
- if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk"
- ~default:false)
- then
- HExtlib.mkdir
- (Filename.dirname
- (Http_getter.filename ~local:true ~writable:true (baseuri ^
- "foo.con")));
- (* begin of compilation *)
let grafite_status = GrafiteSync.init baseuri in
let lexicon_status =
CicNotation2.load_notation ~include_paths:[]
BuildTimeConf.core_notation_script
in
+ let initial_lexicon_status = lexicon_status in
let big_bang = Unix.gettimeofday () in
let time = Unix.time () in
- HLog.message ("compiling " ^ Filename.basename fname ^ " in " ^ baseuri);
- if not (Helm_registry.get_bool "matita.verbose") then
- (let cc =
- if Str.string_match(Str.regexp ".*opt$") Sys.argv.(0) 0 then "matitac.opt"
- else "matitac"
- in
- let s = Printf.sprintf "%s %-35s " cc (cut (root^"/") fname) in
- print_string s; flush stdout);
- let buf = Ulexing.from_utf8_channel (open_in fname) in
- let print_cb =
- if not (Helm_registry.get_bool "matita.verbose") then (fun _ _ -> ())
- else pp_ast_statement
- in
try
+ (* sanity checks *)
+ let moo_fname =
+ LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri ~writable:true
+ in
+ let lexicon_fname=
+ LibraryMisc.lexicon_file_of_baseuri ~must_exist:false ~baseuri ~writable:true
+ in
+ if Http_getter_storage.is_read_only baseuri then
+ HLog.error
+ (Printf.sprintf "uri %s belongs to a read-only repository" baseuri);
+ (* cleanup of previously compiled objects *)
+ if (not (Http_getter_storage.is_empty ~local:true baseuri) ||
+ LibraryClean.db_uris_of_baseuri baseuri <> [])
+ then begin
+ HLog.message ("baseuri " ^ baseuri ^ " is not empty");
+ HLog.message ("cleaning baseuri " ^ baseuri);
+ LibraryClean.clean_baseuris [baseuri];
+ assert (Http_getter_storage.is_empty ~local:true baseuri);
+ end;
+ (* create dir for XML files *)
+ if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk"
+ ~default:false)
+ then
+ HExtlib.mkdir
+ (Filename.dirname
+ (Http_getter.filename ~local:true ~writable:true (baseuri ^
+ "foo.con")));
+ HLog.message ("compiling " ^ Filename.basename fname ^ " in " ^ baseuri);
+ if not (Helm_registry.get_bool "matita.verbose") then
+ (let cc =
+ if Str.string_match(Str.regexp ".*opt$") Sys.argv.(0) 0 then "matitac.opt"
+ else "matitac"
+ in
+ let s = Printf.sprintf "%s %-35s " cc (cut (root^"/") fname) in
+ print_string s; flush stdout);
+ let buf = Ulexing.from_utf8_channel (open_in fname) in
+ let print_cb =
+ if not (Helm_registry.get_bool "matita.verbose") then (fun _ _ -> ())
+ else pp_ast_statement
+ in
let grafite_status, lexicon_status =
match
MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths
with
| [] -> raise End_of_file
| ((grafite,lexicon),None)::_ -> grafite, lexicon
- | (s,Some _)::_ -> raise AttemptToInsertAnAlias
+ | ((_,l),Some _)::_ -> raise (AttemptToInsertAnAlias l)
in
let elapsed = Unix.time () -. time in
let proof_status,moo_content_rev,lexicon_content_rev =
(HLog.error
"there are still incomplete proofs at the end of the script";
pp_times fname false big_bang;
+ LexiconSync.time_travel ~present:lexicon_status ~past:initial_lexicon_status;
clean_exit baseuri false)
else
(if Helm_registry.get_bool "matita.moo" then begin
HLog.message
(sprintf "execution of %s completed in %s." fname (hou^min^sec));
pp_times fname true big_bang;
+ LexiconSync.time_travel ~present:lexicon_status ~past:initial_lexicon_status;
true)
with
- | End_of_file -> HLog.error "End_of_file?!"; clean_exit baseuri false
+ | End_of_file ->
+ HLog.error "End_of_file";
+ pp_times fname false big_bang;
+ clean_exit baseuri false
+ | AttemptToInsertAnAlias lexicon_status ->
+ pp_times fname false big_bang;
+ LexiconSync.time_travel ~present:lexicon_status ~past:initial_lexicon_status;
+ clean_exit baseuri false
| Sys.Break as exn ->
- if matita_debug then raise exn;
+ if matita_debug then raise exn;
HLog.error "user break!";
pp_times fname false big_bang;
clean_exit baseuri false
| GrafiteEngine.Macro (floc, f) ->
- (match f (get_macro_context (Some grafite_status)) with
- | _, GrafiteAst.Inline (_, style, suri, prefix) ->
- let str =
- ApplyTransformation.txt_of_inline_macro style suri prefix
- ~map_unicode_to_tex:(Helm_registry.get_bool
- "matita.paste_unicode_as_tex") in
- !out str;
- compile options fname
- | _ ->
- let x, y = HExtlib.loc_of_floc floc in
- HLog.error (sprintf "A macro has been found at %d-%d" x y);
+ (try
+ match f (get_macro_context (Some grafite_status)) with
+ | _, GrafiteAst.Inline (_, style, suri, prefix) ->
+ let str =
+ ApplyTransformation.txt_of_inline_macro style suri prefix
+ ~map_unicode_to_tex:(Helm_registry.get_bool
+ "matita.paste_unicode_as_tex") in
+ !out str;
+ compile options fname
+ | _ ->
+ let x, y = HExtlib.loc_of_floc floc in
+ HLog.error (sprintf "A macro has been found at %d-%d" x y);
+ pp_times fname false big_bang;
+ clean_exit baseuri false
+ with exn ->
+ HLog.error (snd (MatitaExcPp.to_string exn));
pp_times fname false big_bang;
clean_exit baseuri false)
| HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
pp_times fname false big_bang;
clean_exit baseuri false
| exn ->
- if matita_debug then raise exn;
+ if matita_debug then raise exn;
HLog.error (snd (MatitaExcPp.to_string exn));
pp_times fname false big_bang;
clean_exit baseuri false
-set "baseuri" "cic:/matita/TPTP/BOO001-1".
+
include "logic/equality.ma".
(* Inclusion of: BOO001-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/BOO003-2".
+
include "logic/equality.ma".
(* Inclusion of: BOO003-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/BOO003-4".
+
include "logic/equality.ma".
(* Inclusion of: BOO003-4.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/BOO004-2".
+
include "logic/equality.ma".
(* Inclusion of: BOO004-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/BOO004-4".
+
include "logic/equality.ma".
(* Inclusion of: BOO004-4.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/BOO005-2".
+
include "logic/equality.ma".
(* Inclusion of: BOO005-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/BOO005-4".
+
include "logic/equality.ma".
(* Inclusion of: BOO005-4.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/BOO006-2".
+
include "logic/equality.ma".
(* Inclusion of: BOO006-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/BOO006-4".
+
include "logic/equality.ma".
(* Inclusion of: BOO006-4.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/BOO009-2".
+
include "logic/equality.ma".
(* Inclusion of: BOO009-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/BOO009-4".
+
include "logic/equality.ma".
(* Inclusion of: BOO009-4.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/BOO010-2".
+
include "logic/equality.ma".
(* Inclusion of: BOO010-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/BOO010-4".
+
include "logic/equality.ma".
(* Inclusion of: BOO010-4.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/BOO011-2".
+
include "logic/equality.ma".
(* Inclusion of: BOO011-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/BOO011-4".
+
include "logic/equality.ma".
(* Inclusion of: BOO011-4.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/BOO012-2".
+
include "logic/equality.ma".
(* Inclusion of: BOO012-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/BOO012-4".
+
include "logic/equality.ma".
(* Inclusion of: BOO012-4.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/BOO013-2".
+
include "logic/equality.ma".
(* Inclusion of: BOO013-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/BOO013-4".
+
include "logic/equality.ma".
(* Inclusion of: BOO013-4.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/BOO016-2".
+
include "logic/equality.ma".
(* Inclusion of: BOO016-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/BOO017-2".
+
include "logic/equality.ma".
(* Inclusion of: BOO017-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/BOO018-4".
+
include "logic/equality.ma".
(* Inclusion of: BOO018-4.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/BOO034-1".
+
include "logic/equality.ma".
(* Inclusion of: BOO034-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/BOO069-1".
+
include "logic/equality.ma".
(* Inclusion of: BOO069-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/BOO071-1".
+
include "logic/equality.ma".
(* Inclusion of: BOO071-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/BOO075-1".
+
include "logic/equality.ma".
(* Inclusion of: BOO075-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL004-3".
+
include "logic/equality.ma".
(* Inclusion of: COL004-3.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL007-1".
+
include "logic/equality.ma".
(* Inclusion of: COL007-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL008-1".
+
include "logic/equality.ma".
(* Inclusion of: COL008-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL010-1".
+
include "logic/equality.ma".
(* Inclusion of: COL010-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL012-1".
+
include "logic/equality.ma".
(* Inclusion of: COL012-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL013-1".
+
include "logic/equality.ma".
(* Inclusion of: COL013-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL014-1".
+
include "logic/equality.ma".
(* Inclusion of: COL014-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL015-1".
+
include "logic/equality.ma".
(* Inclusion of: COL015-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL016-1".
+
include "logic/equality.ma".
(* Inclusion of: COL016-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL017-1".
+
include "logic/equality.ma".
(* Inclusion of: COL017-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL018-1".
+
include "logic/equality.ma".
(* Inclusion of: COL018-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL021-1".
+
include "logic/equality.ma".
(* Inclusion of: COL021-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL022-1".
+
include "logic/equality.ma".
(* Inclusion of: COL022-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL024-1".
+
include "logic/equality.ma".
(* Inclusion of: COL024-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL025-1".
+
include "logic/equality.ma".
(* Inclusion of: COL025-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL045-1".
+
include "logic/equality.ma".
(* Inclusion of: COL045-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL048-1".
+
include "logic/equality.ma".
(* Inclusion of: COL048-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL050-1".
+
include "logic/equality.ma".
(* Inclusion of: COL050-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL058-2".
+
include "logic/equality.ma".
(* Inclusion of: COL058-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL058-3".
+
include "logic/equality.ma".
(* Inclusion of: COL058-3.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL060-2".
+
include "logic/equality.ma".
(* Inclusion of: COL060-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL060-3".
+
include "logic/equality.ma".
(* Inclusion of: COL060-3.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL061-2".
+
include "logic/equality.ma".
(* Inclusion of: COL061-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL061-3".
+
include "logic/equality.ma".
(* Inclusion of: COL061-3.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL062-2".
+
include "logic/equality.ma".
(* Inclusion of: COL062-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL062-3".
+
include "logic/equality.ma".
(* Inclusion of: COL062-3.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL063-2".
+
include "logic/equality.ma".
(* Inclusion of: COL063-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL063-3".
+
include "logic/equality.ma".
(* Inclusion of: COL063-3.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL063-4".
+
include "logic/equality.ma".
(* Inclusion of: COL063-4.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL063-5".
+
include "logic/equality.ma".
(* Inclusion of: COL063-5.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL063-6".
+
include "logic/equality.ma".
(* Inclusion of: COL063-6.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL064-2".
+
include "logic/equality.ma".
(* Inclusion of: COL064-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL064-3".
+
include "logic/equality.ma".
(* Inclusion of: COL064-3.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL064-4".
+
include "logic/equality.ma".
(* Inclusion of: COL064-4.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL064-5".
+
include "logic/equality.ma".
(* Inclusion of: COL064-5.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL064-6".
+
include "logic/equality.ma".
(* Inclusion of: COL064-6.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL064-7".
+
include "logic/equality.ma".
(* Inclusion of: COL064-7.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL064-8".
+
include "logic/equality.ma".
(* Inclusion of: COL064-8.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL064-9".
+
include "logic/equality.ma".
(* Inclusion of: COL064-9.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL083-1".
+
include "logic/equality.ma".
(* Inclusion of: COL083-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL084-1".
+
include "logic/equality.ma".
(* Inclusion of: COL084-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL085-1".
+
include "logic/equality.ma".
(* Inclusion of: COL085-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/COL086-1".
+
include "logic/equality.ma".
(* Inclusion of: COL086-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP001-2".
+
include "logic/equality.ma".
(* Inclusion of: GRP001-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP001-4".
+
include "logic/equality.ma".
(* Inclusion of: GRP001-4.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP010-4".
+
include "logic/equality.ma".
(* Inclusion of: GRP010-4.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP011-4".
+
include "logic/equality.ma".
(* Inclusion of: GRP011-4.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP012-4".
+
include "logic/equality.ma".
(* Inclusion of: GRP012-4.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP022-2".
+
include "logic/equality.ma".
(* Inclusion of: GRP022-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP023-2".
+
include "logic/equality.ma".
(* Inclusion of: GRP023-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP115-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP115-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP116-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP116-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP117-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP117-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP118-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP118-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP136-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP136-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP137-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP137-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP139-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP139-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP141-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP141-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP142-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP142-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP143-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP143-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP144-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP144-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP145-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP145-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP146-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP146-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP149-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP149-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP150-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP150-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP151-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP151-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP152-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP152-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP153-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP153-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP154-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP154-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP155-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP155-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP156-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP156-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP157-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP157-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP158-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP158-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP159-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP159-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP160-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP160-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP161-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP161-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP162-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP162-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP163-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP163-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP168-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP168-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP168-2".
+
include "logic/equality.ma".
(* Inclusion of: GRP168-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP173-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP173-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP174-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP174-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP176-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP176-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP176-2".
+
include "logic/equality.ma".
(* Inclusion of: GRP176-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP182-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP182-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP182-2".
+
include "logic/equality.ma".
(* Inclusion of: GRP182-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP182-3".
+
include "logic/equality.ma".
(* Inclusion of: GRP182-3.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP182-4".
+
include "logic/equality.ma".
(* Inclusion of: GRP182-4.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP186-3".
+
include "logic/equality.ma".
(* Inclusion of: GRP186-3.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP186-4".
+
include "logic/equality.ma".
(* Inclusion of: GRP186-4.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP188-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP188-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP188-2".
+
include "logic/equality.ma".
(* Inclusion of: GRP188-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP189-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP189-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP189-2".
+
include "logic/equality.ma".
(* Inclusion of: GRP189-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP192-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP192-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP206-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP206-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP454-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP454-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP455-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP455-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP456-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP456-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP457-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP457-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP458-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP458-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP459-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP459-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP460-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP460-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP463-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP463-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP467-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP467-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP481-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP481-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP484-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP484-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP485-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP485-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP486-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP486-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP487-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP487-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP488-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP488-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP490-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP490-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP491-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP491-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP492-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP492-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP493-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP493-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP494-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP494-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP495-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP495-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP496-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP496-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP497-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP497-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP498-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP498-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP509-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP509-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP510-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP510-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP511-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP511-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP512-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP512-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP513-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP513-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP514-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP514-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP515-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP515-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP516-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP516-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP517-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP517-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP518-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP518-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP520-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP520-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP541-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP541-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP542-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP542-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP543-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP543-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP544-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP544-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP545-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP545-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP546-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP546-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP547-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP547-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP548-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP548-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP549-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP549-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP550-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP550-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP551-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP551-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP552-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP552-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP556-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP556-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP558-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP558-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP560-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP560-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP561-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP561-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP562-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP562-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP564-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP564-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP565-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP565-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP566-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP566-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP567-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP567-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP568-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP568-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP569-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP569-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP570-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP570-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP572-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP572-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP573-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP573-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP574-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP574-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP576-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP576-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP577-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP577-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP578-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP578-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP580-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP580-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP581-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP581-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP582-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP582-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP583-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP583-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP584-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP584-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP586-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP586-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP588-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP588-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP590-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP590-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP592-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP592-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP595-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP595-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP596-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP596-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP597-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP597-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP598-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP598-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP599-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP599-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP600-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP600-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP602-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP602-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP603-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP603-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP604-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP604-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP605-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP605-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP606-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP606-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP608-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP608-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP612-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP612-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP613-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP613-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP614-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP614-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP615-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP615-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/GRP616-1".
+
include "logic/equality.ma".
(* Inclusion of: GRP616-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LAT008-1".
+
include "logic/equality.ma".
(* Inclusion of: LAT008-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LAT033-1".
+
include "logic/equality.ma".
(* Inclusion of: LAT033-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LAT034-1".
+
include "logic/equality.ma".
(* Inclusion of: LAT034-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LAT039-1".
+
include "logic/equality.ma".
(* Inclusion of: LAT039-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LAT039-2".
+
include "logic/equality.ma".
(* Inclusion of: LAT039-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LAT040-1".
+
include "logic/equality.ma".
(* Inclusion of: LAT040-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LAT045-1".
+
include "logic/equality.ma".
(* Inclusion of: LAT045-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LCL110-2".
+
include "logic/equality.ma".
(* Inclusion of: LCL110-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LCL112-2".
+
include "logic/equality.ma".
(* Inclusion of: LCL112-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LCL113-2".
+
include "logic/equality.ma".
(* Inclusion of: LCL113-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LCL114-2".
+
include "logic/equality.ma".
(* Inclusion of: LCL114-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LCL115-2".
+
include "logic/equality.ma".
(* Inclusion of: LCL115-2.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LCL132-1".
+
include "logic/equality.ma".
(* Inclusion of: LCL132-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LCL133-1".
+
include "logic/equality.ma".
(* Inclusion of: LCL133-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LCL134-1".
+
include "logic/equality.ma".
(* Inclusion of: LCL134-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LCL135-1".
+
include "logic/equality.ma".
(* Inclusion of: LCL135-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LCL139-1".
+
include "logic/equality.ma".
(* Inclusion of: LCL139-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LCL140-1".
+
include "logic/equality.ma".
(* Inclusion of: LCL140-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LCL141-1".
+
include "logic/equality.ma".
(* Inclusion of: LCL141-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LCL153-1".
+
include "logic/equality.ma".
(* Inclusion of: LCL153-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LCL154-1".
+
include "logic/equality.ma".
(* Inclusion of: LCL154-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LCL155-1".
+
include "logic/equality.ma".
(* Inclusion of: LCL155-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LCL156-1".
+
include "logic/equality.ma".
(* Inclusion of: LCL156-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LCL157-1".
+
include "logic/equality.ma".
(* Inclusion of: LCL157-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LCL158-1".
+
include "logic/equality.ma".
(* Inclusion of: LCL158-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LCL161-1".
+
include "logic/equality.ma".
(* Inclusion of: LCL161-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LCL164-1".
+
include "logic/equality.ma".
(* Inclusion of: LCL164-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LDA001-1".
+
include "logic/equality.ma".
(* Inclusion of: LDA001-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/LDA007-3".
+
include "logic/equality.ma".
(* Inclusion of: LDA007-3.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/RNG007-4".
+
include "logic/equality.ma".
(* Inclusion of: RNG007-4.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/RNG008-4".
+
include "logic/equality.ma".
(* Inclusion of: RNG008-4.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/RNG011-5".
+
include "logic/equality.ma".
(* Inclusion of: RNG011-5.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/RNG023-6".
+
include "logic/equality.ma".
(* Inclusion of: RNG023-6.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/RNG023-7".
+
include "logic/equality.ma".
(* Inclusion of: RNG023-7.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/RNG024-6".
+
include "logic/equality.ma".
(* Inclusion of: RNG024-6.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/RNG024-7".
+
include "logic/equality.ma".
(* Inclusion of: RNG024-7.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/ROB002-1".
+
include "logic/equality.ma".
(* Inclusion of: ROB002-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/ROB009-1".
+
include "logic/equality.ma".
(* Inclusion of: ROB009-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/ROB010-1".
+
include "logic/equality.ma".
(* Inclusion of: ROB010-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/ROB013-1".
+
include "logic/equality.ma".
(* Inclusion of: ROB013-1.p *)
(* -------------------------------------------------------------------------- *)
-set "baseuri" "cic:/matita/TPTP/ROB030-1".
+
include "logic/equality.ma".
(* Inclusion of: ROB030-1.p *)
(* ------------------------------------------------------------------------------ *)
-set "baseuri" "cic:/matita/TPTP/SYN083-1".
+
include "logic/equality.ma".
(* Inclusion of: SYN083-1.p *)
(* -------------------------------------------------------------------------- *)
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/absurd/".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias num (instance 0) = "natural number".
alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
alias id "not" = "cic:/Coq/Init/Logic/not.con".
(**************************************************************************)
(* test _with_ the WHD on the apply argument *)
-set "baseuri" "cic:/matita/tests/apply/".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias id "not" = "cic:/Coq/Init/Logic/not.con".
alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/apply2".
+
include "nat/nat.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/applys".
+
include "nat/div_and_mod.ma".
include "nat/factorial.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/assumption".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
alias num (instance 0) = "Coq natural number".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/nat/bad_induction".
+
include "nat/nat.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/auto/".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/baseuri/".
-set "baseuri" "cic:/matita/tests/baseuri/".
+
+
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/bool/".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/change/".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias num (instance 0) = "Coq natural number".
alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
alias symbol "plus" (instance 0) = "Coq's natural plus".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/clear".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias num (instance 0) = "natural number".
alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/clearbody".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias num (instance 0) = "Coq natural number".
alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
alias symbol "plus" (instance 0) = "Coq's natural plus".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/coercions/".
+
include "nat/compare.ma".
include "nat/times.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/test/".
+
include "logic/equality.ma".
include "nat/nat.ma".
axiom f : ∀n,m. A n -> B m.
axiom g : ∀n.B n.
-coercion cic:/matita/test/c.con.
-coercion cic:/matita/test/d.con.
+coercion cic:/matita/tests/coercions_contravariant/c.con.
+coercion cic:/matita/tests/coercions_contravariant/d.con.
definition foo := λn,n1,m,m1.(λx.d m m1 (f n m (c n1 n x)) : A1 n1 -> B1 m1).
definition foo1_1 := λn,n1,m,m1.(f n m : A1 n1 -> B1 m1).
definition h := λn,m.λx:A n.g m.
definition foo2 := λn,n1,m,m1.(h n m : A1 n1 -> B1 m1).
definition foo3 := λn1,n,m,m1.(h n m : A1 n1 -> B1 m1).
-definition foo4 := λn1,n,m1,m.(h n m : A1 n1 -> B1 m1).
\ No newline at end of file
+definition foo4 := λn1,n,m1,m.(h n m : A1 n1 -> B1 m1).
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/test/".
+
include "nat/nat.ma".
include "list/list.ma".
axiom veclen : ∀A,n.vec A n -> nat.
-coercion cic:/matita/test/c.con.
+coercion cic:/matita/tests/coercions_dependent/c.con.
alias num (instance 0) = "natural number".
definition xxx := veclen nat ? [3; 4; 7].
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/test/".
+
include "nat/nat.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/test/coercions_nonuniform/".
+
axiom A : Type.
axiom B : A -> Type.
axiom k : ∀a:A.B (f a).
-coercion cic:/matita/test/coercions_nonuniform/k.con.
+coercion cic:/matita/tests/coercions_nonuniform/k.con.
axiom C : Type.
axiom c2 : ∀a.B (f a) -> B (f1 a).
axiom c1 : ∀a:A. B (f1 a) -> C.
-coercion cic:/matita/test/coercions_nonuniform/c1.con.
-coercion cic:/matita/test/coercions_nonuniform/c2.con.
+coercion cic:/matita/tests/coercions_nonuniform/c1.con.
+coercion cic:/matita/tests/coercions_nonuniform/c2.con.
axiom g : C -> C.
(*
Coq < Coercion c1 : B >-> C.
User error: c1 does not respect the inheritance uniform condition
-*)
\ No newline at end of file
+*)
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/test/".
+
include "logic/equality.ma".
include "nat/nat.ma".
axiom jmcBA : ∀n,m.∀p:A n = B m.B m -> A n.
axiom jmcAB : ∀n,m.∀p:A n = B m.A n -> B m.
-coercion cic:/matita/test/jmcAB.con.
-coercion cic:/matita/test/jmcBA.con.
+coercion cic:/matita/tests/coercions_open/jmcAB.con.
+coercion cic:/matita/tests/coercions_open/jmcBA.con.
axiom daemon : ∀x,y:A O.x = y.
alias num (instance 0) = "natural number".
lemma xx : ∀b:B 2.∀a:A 1.eatA ? b = eatB ? a.
intros; [3,5,7,9: apply AB|1: apply daemon];skip.
-qed.
\ No newline at end of file
+qed.
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/test/coercions_propagation/".
+
include "logic/connectives.ma".
include "nat/orders.ma".
sigma_intro: ∀a:A. P a → sigma A P.
interpretation "sigma" 'exists \eta.x =
- (cic:/matita/test/coercions_propagation/sigma.ind#xpointer(1/1) _ x).
+ (cic:/matita/tests/coercions_propagation/sigma.ind#xpointer(1/1) _ x).
definition inject ≝ λP.λa:nat.λp:P a. sigma_intro ? P ? p.
-coercion cic:/matita/test/coercions_propagation/inject.con 0 1.
+coercion cic:/matita/tests/coercions_propagation/inject.con 0 1.
definition eject ≝ λP.λc: ∃n:nat.P n. match c with [ sigma_intro w _ ⇒ w].
-coercion cic:/matita/test/coercions_propagation/eject.con.
+coercion cic:/matita/tests/coercions_propagation/eject.con.
alias num (instance 0) = "natural number".
theorem test: ∃n. 0 ≤ n.
definition injectN ≝ λA,k.λP.λa:NN A k.λp:P a. sigma_intro ? P ? p.
-coercion cic:/matita/test/coercions_propagation/injectN.con 0 1.
+coercion cic:/matita/tests/coercions_propagation/injectN.con 0 1.
definition ejectN ≝ λA,k.λP.λc: ∃n:NN A k.P n. match c with [ sigma_intro w _ ⇒ w].
-coercion cic:/matita/test/coercions_propagation/ejectN.con.
+coercion cic:/matita/tests/coercions_propagation/ejectN.con.
definition PN :=
λA,k.λx:NN A k. 1 <= k.
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/test/russell/".
+
include "nat/orders.ma".
include "list/list.ma".
sig_intro: ∀a:A. P a → sigma A P.
interpretation "sigma" 'exists \eta.x =
- (cic:/matita/test/russell/sigma.ind#xpointer(1/1) _ x).
+ (cic:/matita/tests/coercions_russell/sigma.ind#xpointer(1/1) _ x).
definition inject ≝ λP.λa:list nat.λp:P a. sig_intro ? P ? p.
-coercion cic:/matita/test/russell/inject.con 0 1.
+coercion cic:/matita/tests/coercions_russell/inject.con 0 1.
definition eject ≝ λP.λc: ∃n:list nat.P n. match c with [ sig_intro w _ ⇒ w].
-coercion cic:/matita/test/russell/eject.con.
+coercion cic:/matita/tests/coercions_russell/eject.con.
alias symbol "exists" (instance 2) = "exists".
lemma tl : ∀l:list nat. l ≠ [] → ∃l1.∃a.a :: l1 = l.
definition nat_return := λn:nat. Some ? n.
-coercion cic:/matita/test/russell/nat_return.con.
+coercion cic:/matita/tests/coercions_russell/nat_return.con.
definition raise_exn := None nat.
definition inject_opt ≝ λP.λa:option nat.λp:P a. sig_intro ? P ? p.
-coercion cic:/matita/test/russell/inject_opt.con 0 1.
+coercion cic:/matita/tests/coercions_russell/inject_opt.con 0 1.
definition eject_opt ≝ λP.λc: ∃n:option nat.P n. match c with [ sig_intro w _ ⇒ w].
-coercion cic:/matita/test/russell/eject_opt.con.
+coercion cic:/matita/tests/coercions_russell/eject_opt.con.
(* we may define mem as in the following lemma and get rid of it *)
definition find_spec ≝
notation < "'If' \nbsp b \nbsp 'Then' \nbsp t \nbsp 'Else' \nbsp f" for @{ 'if $b $t $f }.
notation > "'If' b 'Then' t 'Else' f" for @{ 'if $b $t $f }.
-interpretation "if" 'if a b c = (cic:/matita/test/russell/if.con _ a b c).
+interpretation "if" 'if a b c = (cic:/matita/tests/coercions_russell/if.con _ a b c).
definition sigma_find_spec : ∀p,l. sigma ? (λres.find_spec l p res).
(* define the find function *)
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/comments/".
-include "../legacy/coq.ma".
+
+include "coq.ma".
(* commento che va nell'ast, ma non viene contato
come step perche' non e' un executable
-set "baseuri" "cic:/matita/tests/compose/LCL002-1".
+
include "logic/equality.ma".
theorem an_1:
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/constructor".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias num (instance 0) = "natural number".
alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/continuationals".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/contradiction".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
alias id "not" = "cic:/Coq/Init/Logic/not.con".
alias num (instance 0) = "natural number".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/cut".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias num (instance 0) = "natural number".
alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/decl".
+
include "nat/times.ma".
include "nat/orders.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/decompose".
+
include "logic/connectives.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/demodulation/".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias num = "Coq natural number".
alias symbol "times" = "Coq's natural times".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/demodulation_matita/".
+
include "nat/minus.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/dependent_injection".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
alias id "bool" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1)".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/test/dependent_type_inference/".
+
include "nat/nat.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/discriminate".
+
include "logic/equality.ma".
include "nat/nat.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/elim".
-include "../legacy/coq.ma".
+
+include "coq.ma".
inductive stupidtype: Set \def
| Base : stupidtype
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/fguidi/".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
-alias id "le" = "cic:/matita/fguidi/le.ind#xpointer(1/1)".
+alias id "le" = "cic:/matita/tests/fguidi/le.ind#xpointer(1/1)".
alias id "False_ind" = "cic:/Coq/Init/Logic/False_ind.con".
alias id "I" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1/1)".
alias id "ex_intro" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1/1)".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/first/".
+
inductive nat : Set \def
| O : nat
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/fix_betareduction/".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
alias id "n" = "cic:/Suresnes/BDD/canonicite/Canonicity_BDT/n.con".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/fold".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
alias num (instance 0) = "natural number".
alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/generalize".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias num (instance 0) = "Coq natural number".
alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
-set "baseuri" "cic:/matita/TPTP/BOO024-1".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
(* Inclusion of: BOO024-1.p *)
(* -------------------------------------------------------------------------- *)
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/injection".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
alias id "bool" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1)".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/xxx".
+
theorem t: And True (eq nat O O). split. exact (refl_equal nat O). exact I. qed.
\ No newline at end of file
-set "baseuri" "cic:/matita/tests/drop".
+
alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
alias num (instance 0) = "natural number".
-set "baseuri" "cic:/matita/tests/grafite/".
+
(* commento *)
(** hint. *)
-set "baseuri" "cic:/matita/tests/interactive/test5/".
+
whelp instance
\lambda A:Set.
-set "baseuri" "cic:/matita/tests/interactive/test6/".
+
whelp instance
\lambda A:Set.
-set "baseuri" "cic:/matita/tests/interactive/test7/".
+
whelp instance
\lambda A:Set.
-set "baseuri" "cic:/matita/tests/interactive/instance/".
+
whelp instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x:A. P x x.
whelp instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x,y:A. P x y \to P y x.
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/inversion_sum/".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/inversion2/".
-include "../legacy/coq.ma".
+
+include "coq.ma".
inductive nat : Set \def
O : nat
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/letrec/".
+
alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/letrecand".
+
include "nat/nat.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/match_inference/".
+
inductive pos: Set \def
| one : pos
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/metasenv_ordering".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias num (instance 0) = "natural number".
alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/test/".
+
include "logic/equality.ma".
[ exact (C r)
| rewrite > (with_ r); exact (mult (r2_ r))]
qed.
-coercion cic:/matita/test/r2.con.
+coercion cic:/matita/tests/multiple_inheritance/r2.con.
(* convertibility test *)
lemma conv_test : ∀r:R.C r -> K r.
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/mysql_escaping/".
+
theorem a' : Prop \to Prop.intros.assumption.qed.
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/naiveparamod".
+
include "logic/equality.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/test/overred/".
+
include "logic/equality.ma".
axiom t3 : T3.
axiom c : T2 -> X -> X.
-coercion cic:/matita/test/overred/c.con 1.
+coercion cic:/matita/tests/overred/c.con 1.
axiom daemon : c t3 x = x.
theorem find_a_coercion_from_T2_for_a_term_in_T3 : (* c *) t3 x = x.
apply daemon.
-qed.
\ No newline at end of file
+qed.
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/paramodulation".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
alias symbol "plus" (instance 0) = "Coq's natural plus".
-set "baseuri" "cic:/matita/TPTP/BOO075-1".
+
inductive eq (A:Type) (x:A) : A \to Prop \def refl_eq : eq A x x.
qed.
default "equality"
- cic:/matita/TPTP/BOO075-1/eq.ind
- cic:/matita/TPTP/BOO075-1/sym_eq.con
- cic:/matita/TPTP/BOO075-1/trans_eq.con
- cic:/matita/TPTP/BOO075-1/eq_ind.con
- cic:/matita/TPTP/BOO075-1/eq_elim_r.con
- cic:/matita/TPTP/BOO075-1/eq_rec.con
- cic:/matita/TPTP/BOO075-1/eq_elim_r'.con
- cic:/matita/TPTP/BOO075-1/eq_rect.con
- cic:/matita/TPTP/BOO075-1/eq_elim_r''.con
- cic:/matita/TPTP/BOO075-1/eq_f.con
- cic:/matita/TPTP/BOO075-1/eq_f1.con.
+ cic:/matita/tests/paramodulation/BOO075-1/eq.ind
+ cic:/matita/tests/paramodulation/BOO075-1/sym_eq.con
+ cic:/matita/tests/paramodulation/BOO075-1/trans_eq.con
+ cic:/matita/tests/paramodulation/BOO075-1/eq_ind.con
+ cic:/matita/tests/paramodulation/BOO075-1/eq_elim_r.con
+ cic:/matita/tests/paramodulation/BOO075-1/eq_rec.con
+ cic:/matita/tests/paramodulation/BOO075-1/eq_elim_r'.con
+ cic:/matita/tests/paramodulation/BOO075-1/eq_rect.con
+ cic:/matita/tests/paramodulation/BOO075-1/eq_elim_r''.con
+ cic:/matita/tests/paramodulation/BOO075-1/eq_f.con
+ cic:/matita/tests/paramodulation/BOO075-1/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).
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 =
- (cic:/matita/TPTP/BOO075-1/ex.ind#xpointer(1/1) _ x).
+ (cic:/matita/tests/paramodulation/BOO075-1/ex.ind#xpointer(1/1) _ x).
notation < "hvbox(\exists ident i opt (: ty) break . p)"
right associative with precedence 20
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/SK/".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/paramodulation/group".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/paramodulation/irratsqrt2/".
+
include "nat/times.ma".
include "nat/minus.ma".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/pullback".
+
inductive T : Type \def t : T.
inductive L : Type \def l : L.
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/record/".
+
record empty : Type \def {}.
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/replace/".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
alias num (instance 0) = "Coq natural number".
alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/rewrite/".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
alias num (instance 0) = "Coq natural number".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/second/".
+
alias id "nat" = "cic:/matita/tests/first/nat.ind#xpointer(1/1)".
alias id "O" = "cic:/matita/tests/first/nat.ind#xpointer(1/1/1)".
alias id "eq" = "cic:/matita/tests/first/eq.ind#xpointer(1/1)".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/simpl/".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
alias id "plus" = "cic:/Coq/Init/Peano/plus.con".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/test/tacticals".
+
inductive myand (A, B: Prop) : Prop \def
| myconj : ∀a:A.∀b:B. myand A B.
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/test2/".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
alias symbol "and" (instance 0) = "Coq's logical and".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/test3/".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
theorem a:\forall x.x=x.
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/test4/".
-include "../legacy/coq.ma".
+
+include "coq.ma".
(* commento che va nell'ast, ma non viene contato
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/third/".
+
alias id "nat" = "cic:/matita/tests/first/nat.ind#xpointer(1/1)".
alias id "O" = "cic:/matita/tests/first/nat.ind#xpointer(1/1/1)".
alias id "eq" = "cic:/matita/tests/first/eq.ind#xpointer(1/1)".
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/tinycals".
+
theorem prova:
\forall A,B,C:Prop.
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/unfold".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias symbol "plus" (instance 0) = "Coq's natural plus".
definition myplus \def \lambda x,y. x+y.
projects / helm.git / commitdiff