X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda%2Fcube.ma;h=8ac3d978c74f5e6a889cdcc155916c19cf084380;hb=62ba47750dc6a598a01a5c53c375124a517b6ee0;hp=9ddaed35ccb0b6a0dd019ee65daa79cdbf179514;hpb=0f4d8aee837eb33a5598aa0977fc67ec21e8dbf8;p=helm.git diff --git a/matita/matita/lib/lambda/cube.ma b/matita/matita/lib/lambda/cube.ma index 9ddaed35c..8ac3d978c 100644 --- a/matita/matita/lib/lambda/cube.ma +++ b/matita/matita/lib/lambda/cube.ma @@ -17,27 +17,27 @@ include "types.ma". (* PURE TYPE SYSTEMS OF THE λ-CUBE ********************************************) -inductive Cube_Ax (i,j:nat): Prop ≝ - | star_box: i = 0 → j = 1 → Cube_Ax i j +inductive Cube_Ax: nat → nat → Prop ≝ + | star_box: Cube_Ax 0 1 . (* The λPω pure type system (a.k.a. λC or CC) *********************************) -inductive CC_Re (i,j,k:nat): Prop ≝ - | star_star: i = 0 → j = 0 → k = 0 → CC_Re i j k - | box_star : i = 1 → j = 0 → k = 0 → CC_Re i j k - | box_box : i = 1 → j = 1 → k = 1 → CC_Re i j k - | star_box : i = 0 → j = 1 → k = 1 → CC_Re i j k +inductive CC_Re: nat → nat → nat → Prop ≝ + | star_star: CC_Re 0 0 0 + | box_star : CC_Re 1 0 0 + | box_box : CC_Re 1 1 1 + | star_box : CC_Re 0 1 1 . definition CC: pts ≝ mk_pts Cube_Ax CC_Re conv. (* The λω pure type system (a.k.a. Fω) ****************************************) -inductive FO_Re (i,j,k:nat): Prop ≝ - | star_star: i = 0 → j = 0 → k = 0 → FO_Re i j k - | box_star : i = 1 → j = 0 → k = 0 → FO_Re i j k - | box_box : i = 1 → j = 1 → k = 1 → FO_Re i j k +inductive FO_Re: nat → nat → nat → Prop ≝ + | star_star: FO_Re 0 0 0 + | box_star : FO_Re 1 0 0 + | box_box : FO_Re 1 1 1 . definition FO: pts ≝ mk_pts Cube_Ax FO_Re conv.