Function good_basic_def

crates/kernel/src/tutorial/basic.rs:17–29

()

  /// good_def basicDef : Type := Prop
  #[test]
  fn good_basic_def() {
    let mut env = KEnv::<Meta>::new();
    let (id, c) = mk_defn(
      "basicDef",
      0,
      vec![],
      sort1(),
      sort0(),
      ReducibilityHints::Abbrev,
    );
    env.insert(id.clone(), c);
    check_accepts(&mut env, &id);
  }

  /// bad_def badDef : Prop := Type
  /// Value `Type` has type `Type 1`, not `Prop`.