Function mk_thm

crates/kernel/src/testing.rs:156–177

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

}

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

pub fn mk_axiom(
  name: &str,