Function nat_env

crates/kernel/src/inductive.rs:4735–4862

Build env with Nat (1 recursive ctor) and its recursor. Nat : Sort 1 Nat.zero : Nat Nat.succ : Nat → Nat Nat.rec : ∀ (motive : Nat → Sort u) (zero : motive Nat.zero) (succ : ∀ (n : Nat), motive n → motive (Nat.succ n)) (t : Nat), motive t

()

    let mut env = bool_env();
    let mut tc = TypeChecker::new(&mut env);
    assert!(tc.check_const(&mk_id("Bool")).is_ok());
  }

  #[test]
  fn check_inductive_rejects_ctor_param_count_mismatch() {
    let mut env = bool_env();
    env.insert(
      mk_id("Bool.true"),
      KConst::Ctor {
        name: (),
        level_params: (),
        is_unsafe: false,
        lvls: 0,
        induct: mk_id("Bool"),
        cidx: 0,
        params: 1,
        fields: 0,
        ty: cnst("Bool", &[]),
      },
    );

    let mut tc = TypeChecker::new(&mut env);
    match tc.check_const(&mk_id("Bool")) {
      Err(TcError::Other(s)) => assert!(s.contains("ctor params mismatch")),
      other => panic!("expected ctor params mismatch, got {other:?}"),
    }
  }

  #[test]
  fn check_bool_constructor_uses_parent_block() {
    let mut env = bool_env();
    let mut tc = TypeChecker::new(&mut env);
    tc.check_const(&mk_id("Bool.true")).unwrap();
    assert!(
      env.block_check_results.get(&mk_id("Bool")).is_some_and(|r| r.is_ok())
    );
  }

  #[test]
  fn check_bool_rec() {
    let mut env = bool_env();
    let mut tc = TypeChecker::new(&mut env);
    // Must check inductive first to trigger recursor generation
    tc.check_const(&mk_id("Bool")).unwrap();
    assert!(tc.check_const(&mk_id("Bool.rec")).is_ok(), "Bool.rec should pass");
  }

  /// Build env with Nat (1 recursive ctor) and its recursor.
  /// Nat : Sort 1
  /// Nat.zero : Nat
  /// Nat.succ : Nat → Nat
  /// Nat.rec : ∀ (motive : Nat → Sort u) (zero : motive Nat.zero)
  ///             (succ : ∀ (n : Nat), motive n → motive (Nat.succ n))
  ///             (t : Nat), motive t
  fn nat_env() -> KEnv<Anon> {
    let mut env = KEnv::new();
    let block = mk_id("Nat");
    let rec_block = mk_id("Nat.rec.block");