Build Acc inductive environment. Acc : {α : Sort u} → (α → α → Prop) → α → Prop Acc.intro : ∀ {α} {r} {x}, (∀ y, r y x → Acc r y) → Acc r x Acc.rec with k = false (NOT a structure-like recursor)
()
| 413 | let mut env = KEnv::<Meta>::new(); |
| 414 | add_eq_axioms(&mut env); |
| 415 | |
| 416 | // We also need Bool for the reduction test |
| 417 | let bool_id = mk_id("Bool"); |
| 418 | let false_id = mk_id("Bool.false"); |
| 419 | let true_id = mk_id("Bool.true"); |
| 420 | env.insert( |
| 421 | bool_id.clone(), |
| 422 | KConst::Indc { |
| 423 | name: mk_name("Bool"), |
| 424 | level_params: vec![], |
| 425 | lvls: 0, |
| 426 | params: 0, |
| 427 | indices: 0, |
| 428 | is_unsafe: false, |
| 429 | block: bool_id.clone(), |
| 430 | member_idx: 0, |
| 431 | ty: sort1(), |
| 432 | ctors: vec![false_id.clone(), true_id.clone()], |
| 433 | lean_all: vec![bool_id.clone()], |
| 434 | }, |
| 435 | ); |
| 436 | env.insert( |
| 437 | false_id.clone(), |
| 438 | KConst::Ctor { |
| 439 | name: mk_name("Bool.false"), |
| 440 | level_params: vec![], |
| 441 | is_unsafe: false, |
| 442 | lvls: 0, |
| 443 | induct: bool_id.clone(), |
| 444 | cidx: 0, |
| 445 | params: 0, |
| 446 | fields: 0, |
| 447 | ty: cnst("Bool", &[]), |
| 448 | }, |
| 449 | ); |
| 450 | env.insert( |
| 451 | true_id.clone(), |
| 452 | KConst::Ctor { |
| 453 | name: mk_name("Bool.true"), |
| 454 | level_params: vec![], |
| 455 | is_unsafe: false, |
| 456 | lvls: 0, |
| 457 | induct: bool_id.clone(), |
| 458 | cidx: 1, |
| 459 | params: 0, |
| 460 | fields: 0, |
| 461 | ty: cnst("Bool", &[]), |
| 462 | }, |
| 463 | ); |
| 464 | env.blocks.insert(bool_id.clone(), vec![bool_id, false_id, true_id]); |
| 465 | |
| 466 | let n = "Acc"; |
| 467 | let block_id = mk_id(n); |
| 468 | let intro_id = mk_id("Acc.intro"); |
| 469 | let rec_id = mk_id("Acc.rec"); |
| 470 | |
| 471 | // Acc.{u} : {α : Sort u} → (α → α → Prop) → α → Prop |
| 472 | // depth 0: u = param(0) |