Function good_level_comp2

crates/kernel/src/tutorial/basic.rs:228–236

()

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

  /// levelComp3 : Sort 3 := Sort (imax 2 1)
  /// imax 2 1 = max 2 1 = 2, so Sort(imax 2 1) = Sort 2. Sort 2 : Sort 3.