Function good_level_comp3

crates/kernel/src/tutorial/basic.rs:241–249

()

  /// imax 2 1 = max 2 1 = 2, so Sort(imax 2 1) = Sort 2. Sort 2 : Sort 3.
  #[test]
  fn good_level_comp3() {
    let mut env = KEnv::<Meta>::new();
    let ty = sort(usucc(usucc(usucc(uzero())))); // Sort 3
    let val = sort(uimax(usucc(usucc(uzero())), usucc(uzero()))); // Sort (imax 2 1)
    let (id, c) =
      mk_defn("levelComp3", 0, vec![], ty, val, ReducibilityHints::Opaque);
    env.insert(id.clone(), c);
    check_accepts(&mut env, &id);
  }

  /// levelComp4.{u} : Type 0 := Sort (imax u 0)
  /// imax u 0 = 0 for all u (second arg is zero), so Sort(imax u 0) = Prop.