set "baseuri" "cic:/matita/CoRN-Decl/tactics/RingReflection".
+include "CoRN.ma".
+
(* $Id: RingReflection.v,v 1.4 2004/04/23 10:01:06 lcf Exp $ *)
(* begin hide *)
-(* INCLUDE
-CRings
-*)
+include "algebra/CRings.ma".
-(* INCLUDE
-AlgReflection
-*)
+include "tactics/AlgReflection.ma".
(* UNEXPORTED
-Section Ring_Interpretation_Function.
+Section Ring_Interpretation_Function
*)
-inline cic:/CoRN/tactics/RingReflection/R.var.
+alias id "R" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/R.var".
-inline cic:/CoRN/tactics/RingReflection/val.var.
+alias id "val" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/val.var".
-inline cic:/CoRN/tactics/RingReflection/unop.var.
+alias id "unop" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/unop.var".
-inline cic:/CoRN/tactics/RingReflection/binop.var.
+alias id "binop" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/binop.var".
-inline cic:/CoRN/tactics/RingReflection/pfun.var.
+alias id "pfun" = "cic:/CoRN/tactics/RingReflection/Ring_Interpretation_Function/pfun.var".
-inline cic:/CoRN/tactics/RingReflection/interpR.ind.
+inline "cic:/CoRN/tactics/RingReflection/interpR.ind".
-inline cic:/CoRN/tactics/RingReflection/wfR.con.
+inline "cic:/CoRN/tactics/RingReflection/wfR.con".
-inline cic:/CoRN/tactics/RingReflection/xexprR.ind.
+inline "cic:/CoRN/tactics/RingReflection/xexprR.ind".
-inline cic:/CoRN/tactics/RingReflection/xforgetR.con.
+inline "cic:/CoRN/tactics/RingReflection/xforgetR.con".
-inline cic:/CoRN/tactics/RingReflection/xinterpR.con.
+inline "cic:/CoRN/tactics/RingReflection/xinterpR.con".
-inline cic:/CoRN/tactics/RingReflection/xexprR2interpR.con.
+inline "cic:/CoRN/tactics/RingReflection/xexprR2interpR.con".
-inline cic:/CoRN/tactics/RingReflection/xexprR_diagram_commutes.con.
+inline "cic:/CoRN/tactics/RingReflection/xexprR_diagram_commutes.con".
-inline cic:/CoRN/tactics/RingReflection/xexprR2wfR.con.
+inline "cic:/CoRN/tactics/RingReflection/xexprR2wfR.con".
-inline cic:/CoRN/tactics/RingReflection/fexprR.ind.
+inline "cic:/CoRN/tactics/RingReflection/fexprR.ind".
-inline cic:/CoRN/tactics/RingReflection/fexprR_var.con.
+inline "cic:/CoRN/tactics/RingReflection/fexprR_var.con".
-inline cic:/CoRN/tactics/RingReflection/fexprR_int.con.
+inline "cic:/CoRN/tactics/RingReflection/fexprR_int.con".
-inline cic:/CoRN/tactics/RingReflection/fexprR_plus.con.
+inline "cic:/CoRN/tactics/RingReflection/fexprR_plus.con".
-inline cic:/CoRN/tactics/RingReflection/fexprR_mult.con.
+inline "cic:/CoRN/tactics/RingReflection/fexprR_mult.con".
-inline cic:/CoRN/tactics/RingReflection/fforgetR.con.
+inline "cic:/CoRN/tactics/RingReflection/fforgetR.con".
-inline cic:/CoRN/tactics/RingReflection/fexprR2interp.con.
+inline "cic:/CoRN/tactics/RingReflection/fexprR2interp.con".
-inline cic:/CoRN/tactics/RingReflection/fexprR2wf.con.
+inline "cic:/CoRN/tactics/RingReflection/fexprR2wf.con".
(* UNEXPORTED
Opaque csg_crr.
Opaque nexp_op.
*)
-inline cic:/CoRN/tactics/RingReflection/refl_interpR.con.
+inline "cic:/CoRN/tactics/RingReflection/refl_interpR.con".
-inline cic:/CoRN/tactics/RingReflection/interpR_wd.con.
+inline "cic:/CoRN/tactics/RingReflection/interpR_wd.con".
(* UNEXPORTED
-End Ring_Interpretation_Function.
+End Ring_Interpretation_Function
*)
(* UNEXPORTED
-Section Ring_NormCorrect.
+Section Ring_NormCorrect
*)
-inline cic:/CoRN/tactics/RingReflection/R.var.
+alias id "R" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/R.var".
-inline cic:/CoRN/tactics/RingReflection/val.var.
+alias id "val" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/val.var".
-inline cic:/CoRN/tactics/RingReflection/unop.var.
+alias id "unop" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/unop.var".
-inline cic:/CoRN/tactics/RingReflection/binop.var.
+alias id "binop" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/binop.var".
-inline cic:/CoRN/tactics/RingReflection/pfun.var.
+alias id "pfun" = "cic:/CoRN/tactics/RingReflection/Ring_NormCorrect/pfun.var".
+
+(* NOTATION
+Notation II := (interpR R val unop binop pfun).
+*)
(*
four kinds of exprs:
Opaque Zmult.
*)
-inline cic:/CoRN/tactics/RingReflection/MI_mult_corr_R.con.
+inline "cic:/CoRN/tactics/RingReflection/MI_mult_corr_R.con".
(* UNEXPORTED
Transparent Zmult.
Opaque MI_mult.
*)
-inline cic:/CoRN/tactics/RingReflection/MV_mult_corr_R.con.
+inline "cic:/CoRN/tactics/RingReflection/MV_mult_corr_R.con".
(* UNEXPORTED
Transparent MI_mult.
Opaque MV_mult MI_mult.
*)
-inline cic:/CoRN/tactics/RingReflection/MM_mult_corr_R.con.
+inline "cic:/CoRN/tactics/RingReflection/MM_mult_corr_R.con".
(* UNEXPORTED
Transparent MV_mult MI_mult.
Opaque MV_mult.
*)
-inline cic:/CoRN/tactics/RingReflection/MM_plus_corr_R.con.
+inline "cic:/CoRN/tactics/RingReflection/MM_plus_corr_R.con".
(* UNEXPORTED
Transparent MV_mult.
Opaque MM_plus.
*)
-inline cic:/CoRN/tactics/RingReflection/PM_plus_corr_R.con.
+inline "cic:/CoRN/tactics/RingReflection/PM_plus_corr_R.con".
(* UNEXPORTED
Transparent MM_plus.
Opaque PM_plus.
*)
-inline cic:/CoRN/tactics/RingReflection/PP_plus_corr_R.con.
+inline "cic:/CoRN/tactics/RingReflection/PP_plus_corr_R.con".
(* UNEXPORTED
Transparent PM_plus.
Opaque PM_plus MM_mult MI_mult.
*)
-inline cic:/CoRN/tactics/RingReflection/PM_mult_corr_R.con.
+inline "cic:/CoRN/tactics/RingReflection/PM_mult_corr_R.con".
(* UNEXPORTED
Opaque PM_mult.
*)
-inline cic:/CoRN/tactics/RingReflection/PP_mult_corr_R.con.
+inline "cic:/CoRN/tactics/RingReflection/PP_mult_corr_R.con".
(*
Transparent PP_plus PM_mult PP_mult PM_plus MI_mult.
Qed.
*)
-inline cic:/CoRN/tactics/RingReflection/NormR_corr.con.
+inline "cic:/CoRN/tactics/RingReflection/NormR_corr.con".
-inline cic:/CoRN/tactics/RingReflection/Tactic_lemmaR.con.
+inline "cic:/CoRN/tactics/RingReflection/Tactic_lemmaR.con".
(* UNEXPORTED
-End Ring_NormCorrect.
+End Ring_NormCorrect
*)
(* end hide *)