Method try_replace_aux_ref_for_sort

crates/kernel/src/inductive.rs:880–940

(
    &mut self,
    e: &KExpr<M>,
    aux: &[FlatBlockMember<M>],
    aux_ids: &[KId<M>],
    block_us: &[KUniv<M>],
    n_block_params: u64,
    local_depth: u64,
  )

        )?;
        KExpr::let_(n.clone(), ty2, val2, body2, *nd)
      },
      ExprData::Prj(id, field, val, _) => {
        let val2 = self.replace_aux_refs_for_sort(
          val,
          aux,
          aux_ids,
          block_us,
          n_block_params,
          local_depth,
        )?;
        KExpr::prj(id.clone(), *field, val2)
      },
      _ => return Ok(e.clone()),
    };
    Ok(self.env.intern.intern_expr(result))
  }

  fn try_replace_aux_ref_for_sort(
    &mut self,
    e: &KExpr<M>,
    aux: &[FlatBlockMember<M>],
    aux_ids: &[KId<M>],
    block_us: &[KUniv<M>],
    n_block_params: u64,
    local_depth: u64,
  ) -> Result<Option<KExpr<M>>, TcError<M>> {
    let (head, args) = collect_app_spine(e);
    let head_id = match head.data() {
      ExprData::Const(id, _, _) => id,
      _ => return Ok(None),
    };

    for (idx, member) in aux.iter().enumerate() {
      if member.id.addr != head_id.addr {
        continue;
      }
      let own = u64_to_usize::<M>(member.own_params)?;
      if args.len() < own || member.spec_params.len() != own {
        continue;
      }

      let mut matched = true;
      for (arg, sp) in args.iter().take(own).zip(member.spec_params.iter()) {
        let sp_lifted = if local_depth > 0 {
          lift(&mut self.env.intern, sp, local_depth, 0)
        } else {
          sp.clone()
        };
        if !self.is_def_eq(arg, &sp_lifted).unwrap_or(false) {
          matched = false;
          break;
        }
      }
      if !matched {
        continue;
      }

      let anon = || M::meta_field(ix_common::env::Name::anon());