Function
assert_bool_const
(e: &AE, expected: bool, prims: &Primitives<Anon>)
Source from the content-addressed store, hash-verified
| 4774 | let block = mk_id("Nat"); |
| 4775 | |
| 4776 | // Nat : Sort 1 |
| 4777 | env.insert( |
| 4778 | mk_id("Nat"), |
| 4779 | KConst::Indc { |
| 4780 | name: (), |
| 4781 | level_params: (), |
| 4782 | is_unsafe: false, |
| 4783 | lvls: 0, |
| 4784 | params: 0, |
| 4785 | indices: 0, |
| 4786 | block: block.clone(), |
| 4787 | member_idx: 0, |
| 4788 | ty: sort1(), |
| 4789 | ctors: vec![mk_id("Nat.zero"), mk_id("Nat.succ")], |
| 4790 | lean_all: (), |
| 4791 | }, |
| 4792 | ); |
| 4793 | env.insert( |
| 4794 | mk_id("Nat.zero"), |
| 4795 | KConst::Ctor { |
| 4796 | name: (), |