Mimics Std.DHashMap.Raw.WF: Prop inductive with params, index, recursive ctors. Ok.{u} (α : Sort (u+1)) (n : Nat) : Prop Ok.base.{u} : ∀ (α : Sort (u+1)) (n : Nat), Ok.{u} α n Ok.step.{u} : ∀ (α : Sort (u+1)) (n : Nat), Ok.{u} α n → Ok.{u} α n This has 1 univ param, 1 type param, 1 index (Nat), and is in Prop.
()
| 6284 | ExprData::All(_, _, dom, _, _) => dom.clone(), |
| 6285 | _ => panic!("expected forall at binder 9 for cons minor"), |
| 6286 | }; |
| 6287 | // cons minor should have 4 inner binders: |
| 6288 | // ∀ (hd : Inl i) (tl : List (Inl i)) (ih_hd : motive_0 hd) (ih_tl : motive_2 tl), motive_2 (cons (Inl i) hd tl) |
| 6289 | let inner = count_binders(&cons_minor_domain); |
| 6290 | assert_eq!( |
| 6291 | inner, 4, |
| 6292 | "cons minor should have 4 inner binders (2 fields + 2 IH), got {inner}" |
| 6293 | ); |
| 6294 | } |
| 6295 | } |
| 6296 | |
| 6297 | /// Mimics Std.DHashMap.Raw.WF: Prop inductive with params, index, recursive ctors. |
| 6298 | /// |
| 6299 | /// Ok.{u} (α : Sort (u+1)) (n : Nat) : Prop |
| 6300 | /// Ok.base.{u} : ∀ (α : Sort (u+1)) (n : Nat), Ok.{u} α n |
| 6301 | /// Ok.step.{u} : ∀ (α : Sort (u+1)) (n : Nat), Ok.{u} α n → Ok.{u} α n |
| 6302 | /// |
| 6303 | /// This has 1 univ param, 1 type param, 1 index (Nat), and is in Prop. |
| 6304 | fn wf_like_env() -> KEnv<Anon> { |
| 6305 | let mut env = KEnv::new(); |
| 6306 | let block = mk_id("Ok"); |
| 6307 | |
| 6308 | // Nat : Sort 1 |
| 6309 | env.insert( |
| 6310 | mk_id("Nat"), |
| 6311 | KConst::Axio { |
| 6312 | name: (), |
| 6313 | level_params: (), |
| 6314 | is_unsafe: false, |
| 6315 | lvls: 0, |
| 6316 | ty: sort1(), |
| 6317 | }, |
| 6318 | ); |
| 6319 | |
| 6320 | // Ok.{u} : Sort(u+1) → Nat → Prop |
| 6321 | let su = || AU::succ(param(0)); |
| 6322 | let ok_ty = |
| 6323 | pi(AE::sort(su()), pi(cnst("Nat", &[]), KExpr::sort(KUniv::zero()))); |
| 6324 | env.insert( |
| 6325 | mk_id("Ok"), |
| 6326 | KConst::Indc { |
| 6327 | name: (), |
| 6328 | level_params: (), |
| 6329 | lvls: 1, |
| 6330 | params: 1, |
| 6331 | indices: 1, |
| 6332 | is_unsafe: false, |
| 6333 | block: block.clone(), |
| 6334 | member_idx: 0, |
| 6335 | ty: ok_ty, |
| 6336 | ctors: vec![mk_id("Ok.base"), mk_id("Ok.step")], |
| 6337 | lean_all: (), |
| 6338 | }, |
| 6339 | ); |
| 6340 | |
| 6341 | // Ok.base : ∀ (α : Sort(u+1)) (n : Nat), Ok.{u} α n |
| 6342 | let base_ty = pi( |
| 6343 | AE::sort(su()), |