Build Prod.{u,v} : Type u → Type v → Type (max u v) environment.
()
| 1034 | let true_id = mk_id("Bool.true"); |
| 1035 | env.insert( |
| 1036 | bool_id.clone(), |
| 1037 | KConst::Indc { |
| 1038 | name: mk_name("Bool"), |
| 1039 | level_params: vec![], |
| 1040 | lvls: 0, |
| 1041 | params: 0, |
| 1042 | indices: 0, |
| 1043 | is_unsafe: false, |
| 1044 | block: bool_id.clone(), |
| 1045 | member_idx: 0, |
| 1046 | ty: sort1(), |
| 1047 | ctors: vec![false_id.clone(), true_id.clone()], |
| 1048 | lean_all: vec![bool_id.clone()], |
| 1049 | }, |
| 1050 | ); |
| 1051 | env.insert( |
| 1052 | false_id.clone(), |
| 1053 | KConst::Ctor { |
| 1054 | name: mk_name("Bool.false"), |
| 1055 | level_params: vec![], |
| 1056 | is_unsafe: false, |
| 1057 | lvls: 0, |
| 1058 | induct: bool_id.clone(), |
| 1059 | cidx: 0, |
| 1060 | params: 0, |
| 1061 | fields: 0, |
| 1062 | ty: cnst("Bool", &[]), |
| 1063 | }, |
| 1064 | ); |
| 1065 | env.insert( |
| 1066 | true_id.clone(), |
| 1067 | KConst::Ctor { |
| 1068 | name: mk_name("Bool.true"), |
| 1069 | level_params: vec![], |
| 1070 | is_unsafe: false, |
| 1071 | lvls: 0, |
| 1072 | induct: bool_id.clone(), |
| 1073 | cidx: 1, |
| 1074 | params: 0, |
| 1075 | fields: 0, |
| 1076 | ty: cnst("Bool", &[]), |
| 1077 | }, |
| 1078 | ); |
| 1079 | env.blocks.insert(bool_id, vec![mk_id("Bool"), false_id, true_id]); |
| 1080 | |
| 1081 | let n = "Prod"; |
| 1082 | let block_id = mk_id(n); |
| 1083 | let mk_ctor_id = mk_id("Prod.mk"); |
| 1084 | let rec_ctor_id = mk_id("Prod.rec"); |
| 1085 | |
| 1086 | // Prod.{u,v} : Type u → Type v → Type (max u v) |
| 1087 | // param(0) = u, param(1) = v |
| 1088 | let prod_ty = npi( |
| 1089 | "α", |
| 1090 | sort(usucc(param(0))), |
| 1091 | npi("β", sort(usucc(param(1))), sort(usucc(umax(param(0), param(1))))), |
| 1092 | ); |
| 1093 | env.insert( |