Function lean_axio

crates/kernel/src/congruence.rs:695–704

(
    name: &str,
    lvls: Vec<Name>,
    typ: env::Expr,
  )

  // ---- const_congruent ----

  fn lean_axio(
    name: &str,
    lvls: Vec<Name>,
    typ: env::Expr,
  ) -> env::ConstantInfo {
    env::ConstantInfo::AxiomInfo(AxiomVal {
      cnst: ConstantVal { name: mk_name(name), level_params: lvls, typ },
      is_unsafe: false,
    })
  }

  fn zero_axio(lvls: u64, ty: KExpr<Anon>) -> KConst<Anon> {
    KConst::Axio { name: (), level_params: (), is_unsafe: false, lvls, ty }