Method inductive_app_is_prop

crates/kernel/src/infer.rs:486–518

(
    &mut self,
    ind_id: &KId<M>,
    levels: &[KUniv<M>],
    binders: usize,
  )

  fn inductive_app_is_prop(
    &mut self,
    ind_id: &KId<M>,
    levels: &[KUniv<M>],
    binders: usize,
  ) -> Result<bool, TcError<M>> {
    use super::level::{KUniv, univ_eq};

    let ind_ty = match self.try_get_const(ind_id)? {
      Some(KConst::Indc { ty, .. }) => ty,
      _ => {
        return Err(TcError::Other("projection: not an inductive type".into()));
      },
    };
    let levels_vec: Vec<_> = levels.to_vec();
    let mut r = self.instantiate_univ_params(&ind_ty, &levels_vec)?;
    for _ in 0..binders {
      let wr = self.whnf(&r)?;
      match wr.data() {
        ExprData::All(_, _, _, body, _) => {
          r = body.clone();
        },
        _ => {
          return Err(TcError::Other(
            "projection: expected forall in inductive type".into(),
          ));
        },
      }
    }
    let sort_ty = self.whnf(&r)?;
    let level = self.ensure_sort(&sort_ty)?;
    Ok(univ_eq(&level, &KUniv::zero()))
  }
}

fn compact_expr<M: KernelMode>(e: &KExpr<M>) -> String {
  compact_expr_deep(e, 1)