Function test_roundtrip_inductive_simple

crates/compile/src/compile.rs:5510–5590

()

    let def = DefinitionVal {
      cnst,
      value,
      hints: ReducibilityHints::Abbrev,
      safety: DefinitionSafety::Safe,
      all: vec![name.clone()],
    };

    let mut lean_env = LeanEnv::default();
    lean_env.insert(name.clone(), LeanConstantInfo::DefnInfo(def));
    let lean_env = Arc::new(lean_env);

    let stt = CompileState::default();
    let mut cache = BlockCache::default();
    let mut all = NameSet::default();
    all.insert(name.clone());

    // This should work because it's a single self-referential def
    let result = compile_const(
      &name,
      &all,
      &lean_env,
      &mut cache,
      &stt,
      &mut KernelCtx::new(),
    );
    assert!(result.is_ok(), "compile_const failed: {:?}", result.err());

    let addr = result.unwrap();
    assert!(stt.name_to_addr.contains_key(&name));

    // Check the constant was stored
    let cnst = stt.env.get_const(&addr);
    assert!(cnst.is_some());
    match cnst.unwrap().as_ref() {
      Constant { info: ConstantInfo::Defn(d), .. } => {
        // Value should be a Rec(0) since it's self-referential in a single-element block
        match d.value.as_ref() {
          Expr::Rec(0, _) => {}, // Expected
          other => panic!("Expected Rec(0), got {:?}", other),
        }
      },
      other => panic!("Expected Defn, got {:?}", other),
    }
  }

  #[test]
  fn test_compile_env_single_axiom() {
    use ix_common::env::{AxiomVal, ConstantVal};

    // Create a minimal environment with just one axiom
    let name = Name::str(Name::anon(), "myAxiom".to_string());
    let typ = LeanExpr::sort(Level::succ(Level::zero())); // Type 0
    let cnst = ConstantVal { name: name.clone(), level_params: vec![], typ };
    let axiom = AxiomVal { cnst, is_unsafe: false };

    let mut lean_env = LeanEnv::default();
    lean_env.insert(name.clone(), LeanConstantInfo::AxiomInfo(axiom));
    let lean_env = Arc::new(lean_env);