Function good_level_comp1

crates/kernel/src/tutorial/basic.rs:214–222

()

  /// But type is Sort 1 = Type, so Prop : Type is correct.
  #[test]
  fn good_level_comp1() {
    let mut env = KEnv::<Meta>::new();
    let ty = sort(usucc(uzero())); // Sort 1
    let val = sort(uimax(usucc(uzero()), uzero())); // Sort (imax 1 0)
    let (id, c) =
      mk_defn("levelComp1", 0, vec![], ty, val, ReducibilityHints::Opaque);
    env.insert(id.clone(), c);
    check_accepts(&mut env, &id);
  }

  /// levelComp2 : Sort 2 := Sort (imax 0 1)
  /// imax 0 1 = max 0 1 = 1 (since second arg is nonzero), so Sort(imax 0 1) = Sort 1 = Type.