Build an environment with Bool + RTree (reflexive inductive). RTree : Type, RTree.leaf : RTree, RTree.node : (Bool → RTree) → RTree
()
| 736 | let block_id = mk_id(n); |
| 737 | let leaf_id = mk_id("RTree.leaf"); |
| 738 | let node_id = mk_id("RTree.node"); |
| 739 | let rec_id = mk_id("RTree.rec"); |
| 740 | |
| 741 | let rt = || cnst(n, &[]); |
| 742 | |
| 743 | // RTree : Type |
| 744 | env.insert( |
| 745 | block_id.clone(), |
| 746 | KConst::Indc { |
| 747 | name: mk_name(n), |
| 748 | level_params: vec![], |
| 749 | lvls: 0, |
| 750 | params: 0, |
| 751 | indices: 0, |
| 752 | is_unsafe: false, |
| 753 | block: block_id.clone(), |
| 754 | member_idx: 0, |
| 755 | ty: sort1(), |
| 756 | ctors: vec![leaf_id.clone(), node_id.clone()], |
| 757 | lean_all: vec![block_id.clone()], |
| 758 | }, |
| 759 | ); |
| 760 | |
| 761 | // RTree.leaf : RTree |
| 762 | env.insert( |
| 763 | leaf_id.clone(), |
| 764 | KConst::Ctor { |
| 765 | name: mk_name("RTree.leaf"), |
| 766 | level_params: vec![], |
| 767 | is_unsafe: false, |
| 768 | lvls: 0, |
| 769 | induct: block_id.clone(), |
| 770 | cidx: 0, |
| 771 | params: 0, |
| 772 | fields: 0, |
| 773 | ty: rt(), |
| 774 | }, |
| 775 | ); |
| 776 | |
| 777 | // RTree.node : (Bool → RTree) → RTree |
| 778 | env.insert( |
| 779 | node_id.clone(), |
| 780 | KConst::Ctor { |
| 781 | name: mk_name("RTree.node"), |
| 782 | level_params: vec![], |
| 783 | is_unsafe: false, |
| 784 | lvls: 0, |
| 785 | induct: block_id.clone(), |
| 786 | cidx: 1, |
| 787 | params: 0, |
| 788 | fields: 1, |
| 789 | ty: npi("children", pi(cnst("Bool", &[]), rt()), rt()), |
| 790 | }, |
| 791 | ); |
| 792 | |
| 793 | // RTree.rec : ∀ {motive : RTree → Sort u} |
| 794 | // (leaf : motive RTree.leaf) |
| 795 | // (node : ∀ (children : Bool → RTree), (∀ b, motive (children b)) → motive (RTree.node children)) |