X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FBasics.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FBasics.ma;h=22f1f819a59b0df0de278501f96ed4580ec9b287;hb=80110e17ef1d38d71473e9471ce15beddde663bb;hp=8794b52cc732184ca9aa34ed827c8b4fb2d37a54;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/Basics.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/Basics.ma index 8794b52cc..22f1f819a 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/Basics.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/Basics.ma @@ -16,6 +16,8 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/Basics". +include "CoRN.ma". + (* $Id: Basics.v,v 1.7 2004/04/09 15:58:31 lcf Exp $ *) (*#* printing alpha %\ensuremath{\alpha}% #α# *) @@ -36,50 +38,32 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/Basics". (*#* printing Z %\ensuremath{\mathbb Z}% #Z# *) -(* INCLUDE -Omega -*) - -(* INCLUDE -Even -*) - -(* INCLUDE -Max -*) - -(* INCLUDE -Min -*) - -(* INCLUDE -ListType -*) +include "algebra/ListType.ma". (*#* *Basics This is random stuff that should be in the Coq basic library. *) -inline cic:/CoRN/algebra/Basics/lt_le_dec.con. +inline "cic:/CoRN/algebra/Basics/lt_le_dec.con". -inline cic:/CoRN/algebra/Basics/lt_z_two.con. +inline "cic:/CoRN/algebra/Basics/lt_z_two.con". -inline cic:/CoRN/algebra/Basics/le_pred.con. +inline "cic:/CoRN/algebra/Basics/le_pred.con". -inline cic:/CoRN/algebra/Basics/lt_mult_right.con. +inline "cic:/CoRN/algebra/Basics/lt_mult_right.con". -inline cic:/CoRN/algebra/Basics/le_mult_right.con. +inline "cic:/CoRN/algebra/Basics/le_mult_right.con". (*#* The power function does not exist in the standard library *) -inline cic:/CoRN/algebra/Basics/power.con. +inline "cic:/CoRN/algebra/Basics/power.con". (*#* Factorial function. Does not exist in Arith. Needed for special operations on polynomials. *) -inline cic:/CoRN/algebra/Basics/fac.con. +inline "cic:/CoRN/algebra/Basics/fac.con". -inline cic:/CoRN/algebra/Basics/nat_fac_gtzero.con. +inline "cic:/CoRN/algebra/Basics/nat_fac_gtzero.con". (* needed for computational behavior of "Inversion" tactic *) @@ -125,9 +109,9 @@ Intros. Right. Reflexivity. Qed. *) -inline cic:/CoRN/algebra/Basics/not_r_sumbool_rec.con. +inline "cic:/CoRN/algebra/Basics/not_r_sumbool_rec.con". -inline cic:/CoRN/algebra/Basics/not_l_sumbool_rec.con. +inline "cic:/CoRN/algebra/Basics/not_l_sumbool_rec.con". (* begin hide *) @@ -148,33 +132,35 @@ coercion. *) (* begin hide *) +coercion "cic:/matita/CoRN-Decl/algebra/Basics/Z_of_nat.con" 0 (* compounds *). + (* end hide *) -inline cic:/CoRN/algebra/Basics/POS_anti_convert.con. +inline "cic:/CoRN/algebra/Basics/POS_anti_convert.con". -inline cic:/CoRN/algebra/Basics/NEG_anti_convert.con. +inline "cic:/CoRN/algebra/Basics/NEG_anti_convert.con". -inline cic:/CoRN/algebra/Basics/lt_O_positive_to_nat.con. +inline "cic:/CoRN/algebra/Basics/lt_O_positive_to_nat.con". -inline cic:/CoRN/algebra/Basics/anti_convert_pred_convert.con. +inline "cic:/CoRN/algebra/Basics/anti_convert_pred_convert.con". -inline cic:/CoRN/algebra/Basics/p_is_some_anti_convert.con. +inline "cic:/CoRN/algebra/Basics/p_is_some_anti_convert.con". -inline cic:/CoRN/algebra/Basics/convert_is_POS.con. +inline "cic:/CoRN/algebra/Basics/convert_is_POS.con". -inline cic:/CoRN/algebra/Basics/min_convert_is_NEG.con. +inline "cic:/CoRN/algebra/Basics/min_convert_is_NEG.con". -inline cic:/CoRN/algebra/Basics/inject_nat_convert.con. +inline "cic:/CoRN/algebra/Basics/inject_nat_convert.con". -inline cic:/CoRN/algebra/Basics/Z_exh.con. +inline "cic:/CoRN/algebra/Basics/Z_exh.con". -inline cic:/CoRN/algebra/Basics/nats_Z_ind.con. +inline "cic:/CoRN/algebra/Basics/nats_Z_ind.con". -inline cic:/CoRN/algebra/Basics/pred_succ_Z_ind.con. +inline "cic:/CoRN/algebra/Basics/pred_succ_Z_ind.con". -inline cic:/CoRN/algebra/Basics/Zmult_minus_distr_r.con. +inline "cic:/CoRN/algebra/Basics/Zmult_minus_distr_r.con". -inline cic:/CoRN/algebra/Basics/Zodd_Zeven_min1.con. +inline "cic:/CoRN/algebra/Basics/Zodd_Zeven_min1.con". (* begin hide *) @@ -188,7 +174,7 @@ Unset Strict Implicit. (* end hide *) -inline cic:/CoRN/algebra/Basics/caseZ_diff.con. +inline "cic:/CoRN/algebra/Basics/caseZ_diff.con". (* begin hide *) @@ -202,37 +188,37 @@ Unset Implicit Arguments. (* end hide *) -inline cic:/CoRN/algebra/Basics/caseZ_diff_O.con. +inline "cic:/CoRN/algebra/Basics/caseZ_diff_O.con". -inline cic:/CoRN/algebra/Basics/caseZ_diff_Pos.con. +inline "cic:/CoRN/algebra/Basics/caseZ_diff_Pos.con". -inline cic:/CoRN/algebra/Basics/caseZ_diff_Neg.con. +inline "cic:/CoRN/algebra/Basics/caseZ_diff_Neg.con". -inline cic:/CoRN/algebra/Basics/proper_caseZ_diff.con. +inline "cic:/CoRN/algebra/Basics/proper_caseZ_diff.con". -inline cic:/CoRN/algebra/Basics/diff_Z_ind.con. +inline "cic:/CoRN/algebra/Basics/diff_Z_ind.con". -inline cic:/CoRN/algebra/Basics/Zlt_reg_mult_l.con. +inline "cic:/CoRN/algebra/Basics/Zlt_reg_mult_l.con". -inline cic:/CoRN/algebra/Basics/Zlt_opp.con. +inline "cic:/CoRN/algebra/Basics/Zlt_opp.con". -inline cic:/CoRN/algebra/Basics/Zlt_conv_mult_l.con. +inline "cic:/CoRN/algebra/Basics/Zlt_conv_mult_l.con". -inline cic:/CoRN/algebra/Basics/Zgt_not_eq.con. +inline "cic:/CoRN/algebra/Basics/Zgt_not_eq.con". -inline cic:/CoRN/algebra/Basics/Zmult_absorb.con. +inline "cic:/CoRN/algebra/Basics/Zmult_absorb.con". (* UNEXPORTED Section Well_foundedT. *) -inline cic:/CoRN/algebra/Basics/A.var. +inline "cic:/CoRN/algebra/Basics/A.var". -inline cic:/CoRN/algebra/Basics/R.var. +inline "cic:/CoRN/algebra/Basics/R.var". (*#* The accessibility predicate is defined to be non-informative *) -inline cic:/CoRN/algebra/Basics/Acc.ind. +inline "cic:/CoRN/algebra/Basics/Acc.ind". (* UNEXPORTED End Well_foundedT. @@ -242,9 +228,9 @@ End Well_foundedT. Section AccT. *) -inline cic:/CoRN/algebra/Basics/A.var. +inline "cic:/CoRN/algebra/Basics/A.var". -inline cic:/CoRN/algebra/Basics/well_founded.con. +inline "cic:/CoRN/algebra/Basics/well_founded.con". (* UNEXPORTED End AccT. @@ -258,29 +244,29 @@ Implicit Arguments Acc [A]. Section IndT. *) -inline cic:/CoRN/algebra/Basics/A.var. +inline "cic:/CoRN/algebra/Basics/A.var". -inline cic:/CoRN/algebra/Basics/R.var. +inline "cic:/CoRN/algebra/Basics/R.var". (* UNEXPORTED Section AccIter. *) -inline cic:/CoRN/algebra/Basics/P.var. +inline "cic:/CoRN/algebra/Basics/P.var". -inline cic:/CoRN/algebra/Basics/F.var. +inline "cic:/CoRN/algebra/Basics/F.var". -inline cic:/CoRN/algebra/Basics/Acc_inv.con. +inline "cic:/CoRN/algebra/Basics/Acc_inv.con". -inline cic:/CoRN/algebra/Basics/Acc_iter.con. +inline "cic:/CoRN/algebra/Basics/Acc_iter.con". (* UNEXPORTED End AccIter. *) -inline cic:/CoRN/algebra/Basics/Rwf.var. +inline "cic:/CoRN/algebra/Basics/Rwf.var". -inline cic:/CoRN/algebra/Basics/well_founded_induction_type.con. +inline "cic:/CoRN/algebra/Basics/well_founded_induction_type.con". (* UNEXPORTED End IndT. @@ -290,15 +276,15 @@ End IndT. Section InductionT. *) -inline cic:/CoRN/algebra/Basics/A.var. +inline "cic:/CoRN/algebra/Basics/A.var". -inline cic:/CoRN/algebra/Basics/f.var. +inline "cic:/CoRN/algebra/Basics/f.var". -inline cic:/CoRN/algebra/Basics/ltof.con. +inline "cic:/CoRN/algebra/Basics/ltof.con". -inline cic:/CoRN/algebra/Basics/well_founded_ltof.con. +inline "cic:/CoRN/algebra/Basics/well_founded_ltof.con". -inline cic:/CoRN/algebra/Basics/induction_ltof2T.con. +inline "cic:/CoRN/algebra/Basics/induction_ltof2T.con". (* UNEXPORTED End InductionT. @@ -308,7 +294,7 @@ End InductionT. Section InductionTT. *) -inline cic:/CoRN/algebra/Basics/lt_wf_rect.con. +inline "cic:/CoRN/algebra/Basics/lt_wf_rect.con". (* UNEXPORTED End InductionTT.