Function recursor_refs_rules

crates/compile/src/graph.rs:384–425

()

      ConstantInfo::CtorInfo(ConstructorVal {
        cnst: mk_cv("T.mk2"),
        induct: n("T"),
        cidx: Nat::from(1u64),
        num_params: Nat::from(0u64),
        num_fields: Nat::from(0u64),
        is_unsafe: false,
      }),
    );

    let graph = build_ref_graph(&env);
    // T references T.mk1 and T.mk2 (from ctors list)
    assert!(graph.out_refs[&n("T")].contains(&n("T.mk1")));
    assert!(graph.out_refs[&n("T")].contains(&n("T.mk2")));
  }

  #[test]
  fn inductive_all_members_are_not_graph_edges() {
    // `InductiveVal.all` is Lean source metadata. The canonical compiler
    // must still split inductive declarations into their minimal SCCs, so
    // members that do not structurally reference each other are not graph
    // dependencies merely because Lean recorded them in the same `all` list.
    let mut env = Env::default();
    for name in ["A", "B"] {
      env.insert(
        n(name),
        ConstantInfo::InductInfo(InductiveVal {
          cnst: mk_cv(name),
          num_params: Nat::from(0u64),
          num_indices: Nat::from(0u64),
          all: vec![n("A"), n("B")],
          ctors: vec![],
          num_nested: Nat::from(0u64),
          is_rec: false,
          is_unsafe: false,
          is_reflexive: false,
        }),
      );
    }

    let graph = build_ref_graph(&env);
    assert!(!graph.out_refs[&n("A")].contains(&n("B")));
    assert!(!graph.out_refs[&n("B")].contains(&n("A")));
  }

  #[test]
  fn ctor_includes_induct() {