Method check_param_agreement

crates/kernel/src/inductive.rs:1661–1700

A1: Check that the first `n_params` forall domains of ind_ty and ctor_ty agree.

(
    &mut self,
    ind_ty: &KExpr<M>,
    ctor_ty: &KExpr<M>,
    n_params: usize,
  )

      log::info!("  sto: {rhs}");
      return Ok(true);
    }

    let lw = self.whnf(lhs)?;
    let rw = self.whnf(rhs)?;
    match (lw.data(), rw.data()) {
      (
        ExprData::Lam(_, _, lty, lbody, _),
        ExprData::Lam(_, _, rty, rbody, _),
      )
      | (
        ExprData::All(_, _, lty, lbody, _),
        ExprData::All(_, _, rty, rbody, _),
      ) => {
        if !self.is_def_eq(lty, rty)? {
          log::info!("[rule rhs diff] first diff {path}.dom");
          log::info!("  gen: {lty}");
          log::info!("  sto: {rty}");
          return Ok(true);
        }
        let saved = self.lctx.len();
        let (lbody_open, fv, _) =
          self.open_binder_anon_with_fv(lty.clone(), lbody);
        let rbody_open = instantiate_rev(&mut self.env.intern, rbody, &[fv]);
        let found = self.dump_rule_rhs_first_diff(
          &lbody_open,
          &rbody_open,
          &format!("{path}.body"),
          depth + 1,
        );
        self.lctx.truncate(saved);
        found
      },
      (ExprData::App(lf, la, _), ExprData::App(rf, ra, _)) => {
        if self.dump_rule_rhs_first_diff(
          lf,
          rf,
          &format!("{path}.fn"),
          depth + 1,
        )? {
          return Ok(true);
        }
        self.dump_rule_rhs_first_diff(la, ra, &format!("{path}.arg"), depth + 1)
      },