Method count_foralls

crates/kernel/src/check.rs:732–759

Count the number of leading foralls in a type.

(&mut self, ty: &KExpr<M>)

          if u64_to_usize::<M>(c.lvls())? != us.len() {
            return Err(TcError::UnivParamMismatch {
              expected: c.lvls(),
              got: us.len(),
            });
          }
          for u in us {
            let univ_start = timing.as_ref().map(|_| Instant::now());
            self.validate_univ_params_seen(u, lvl_bound, &mut seen_univs)?;
            if let (Some(t), Some(start)) = (timing.as_deref_mut(), univ_start)
            {
              t.univ += start.elapsed();
            }
          }
        },
        ExprData::App(f, a, _) => {
          stack.push((f, depth));
          stack.push((a, depth));
        },
        ExprData::Lam(_, _, ty, body, _) | ExprData::All(_, _, ty, body, _) => {
          stack.push((ty, depth));
          let body_depth = depth.checked_add(1).ok_or_else(|| {
            TcError::Other("binder depth overflow during validation".into())
          })?;
          stack.push((body, body_depth));
        },
        ExprData::Let(_, ty, val, body, _, _) => {
          stack.push((ty, depth));
          stack.push((val, depth));
          let body_depth = depth.checked_add(1).ok_or_else(|| {
            TcError::Other("binder depth overflow during validation".into())
          })?;
          stack.push((body, body_depth));