| 273 | /// Sort u : Type u = Sort (u+1). |
| 274 | #[test] |
| 275 | fn good_level_comp5() { |
| 276 | let mut env = KEnv::<Meta>::new(); |
| 277 | let ty = sort(usucc(param(0))); // Type u = Sort (u+1) |
| 278 | let val = sort(uimax(param(0), param(0))); // Sort (imax u u) |
| 279 | let (id, c) = mk_defn( |
| 280 | "levelComp5", |
| 281 | 1, |
| 282 | vec![mk_name("u")], |
| 283 | ty, |
| 284 | val, |
| 285 | ReducibilityHints::Abbrev, |
| 286 | ); |
| 287 | env.insert(id.clone(), c); |
| 288 | check_accepts(&mut env, &id); |
| 289 | } |
| 290 | |
| 291 | /// imax1 : (p : Prop) → Prop := fun p => Type → p |
| 292 | /// Inside the lambda, p : Prop, so (Type → p) : Sort(imax 2 1) but |