Build a PUnit-like unit type environment. MyUnit : Type, MyUnit.star : MyUnit, MyUnit.rec
()
| 285 | /// Build a PUnit-like unit type environment. |
| 286 | /// MyUnit : Type, MyUnit.star : MyUnit, MyUnit.rec |
| 287 | fn unit_env() -> KEnv<Meta> { |
| 288 | let mut env = KEnv::<Meta>::new(); |
| 289 | let n = "MyUnit"; |
| 290 | let block_id = mk_id(n); |
| 291 | let ctor_id = mk_id(&format!("{n}.star")); |
| 292 | let rec_id = mk_id(&format!("{n}.rec")); |
| 293 | |
| 294 | // MyUnit : Type |
| 295 | env.insert( |
| 296 | block_id.clone(), |
| 297 | KConst::Indc { |
| 298 | name: mk_name(n), |
| 299 | level_params: vec![], |
| 300 | lvls: 0, |
| 301 | params: 0, |
| 302 | indices: 0, |
| 303 | is_unsafe: false, |
| 304 | block: block_id.clone(), |
| 305 | member_idx: 0, |
| 306 | ty: sort1(), |
| 307 | ctors: vec![ctor_id.clone()], |
| 308 | lean_all: vec![block_id.clone()], |
| 309 | }, |
| 310 | ); |
| 311 | |
| 312 | // MyUnit.star : MyUnit |
| 313 | env.insert( |
| 314 | ctor_id.clone(), |
| 315 | KConst::Ctor { |
| 316 | name: mk_name(&format!("{n}.star")), |
| 317 | level_params: vec![], |
| 318 | is_unsafe: false, |
| 319 | lvls: 0, |
| 320 | induct: block_id.clone(), |
| 321 | cidx: 0, |
| 322 | params: 0, |
| 323 | fields: 0, |
| 324 | ty: cnst(n, &[]), |
| 325 | }, |
| 326 | ); |
| 327 | |
| 328 | // MyUnit.rec : ∀ {motive : MyUnit → Sort u} (star : motive MyUnit.star) (t : MyUnit), motive t |
| 329 | let motive_ty = pi(cnst(n, &[]), sort(param(0))); |
| 330 | let minor_star = app(var(0), cnst(&format!("{n}.star"), &[])); |
| 331 | let rec_ty = ipi( |
| 332 | "motive", |
| 333 | motive_ty, |
| 334 | npi( |
| 335 | "star", |
| 336 | minor_star.clone(), |
| 337 | npi("t", cnst(n, &[]), app(var(2), var(0))), |
| 338 | ), |
| 339 | ); |
| 340 | |
| 341 | // Rule: star case → λ motive star_val, star_val |
| 342 | let rule_rhs = nlam( |
| 343 | "motive", |
| 344 | pi(cnst(n, &[]), sort(param(0))), |