Function mk_defn

crates/kernel/src/testing.rs:132–154

(
  name: &str,
  lvls: u64,
  level_params: Vec<Name>,
  ty: ME,
  val: ME,
  hints: ReducibilityHints,
)

// ---- Constant builders ----

pub fn mk_defn(
  name: &str,
  lvls: u64,
  level_params: Vec<Name>,
  ty: ME,
  val: ME,
  hints: ReducibilityHints,
) -> (MId, KConst<Meta>) {
  let id = mk_id(name);
  let c = KConst::Defn {
    name: mk_name(name),
    level_params,
    kind: DefKind::Definition,
    safety: DefinitionSafety::Safe,
    hints,
    lvls,
    ty,
    val,
    lean_all: vec![id.clone()],
    block: id.clone(),
  };
  (id, c)
}

pub fn mk_thm(
  name: &str,