Function inductive_includes_ctors

crates/compile/src/graph.rs:250–295

()

      let f_name_set = get_expr_references(f, cache);
      let a_name_set = get_expr_references(a, cache);
      merge_name_sets(f_name_set, a_name_set)
    },
    ExprData::Lam(_, typ, body, ..) | ExprData::ForallE(_, typ, body, ..) => {
      let typ_name_set = get_expr_references(typ, cache);
      let body_name_set = get_expr_references(body, cache);
      merge_name_sets(typ_name_set, body_name_set)
    },
    ExprData::LetE(_, typ, value, body, ..) => {
      let typ_name_set = get_expr_references(typ, cache);
      let value_name_set = get_expr_references(value, cache);
      let body_name_set = get_expr_references(body, cache);
      merge_name_sets(
        typ_name_set,
        merge_name_sets(value_name_set, body_name_set),
      )
    },
    ExprData::Mdata(_, expr, _) => get_expr_references(expr, cache),
    ExprData::Proj(type_name, _, expr, _) => {
      let mut name_set = get_expr_references(expr, cache);
      name_set.insert(type_name.clone());
      name_set
    },
    _ => NameSet::default(),
  };
  cache.insert(expr, name_set.clone());
  name_set
}

#[cfg(test)]
mod tests {
  use super::*;
  use bignat::Nat;
  use ix_common::env::*;

  fn n(s: &str) -> Name {
    Name::str(Name::anon(), s.to_string())
  }

  fn sort0() -> Expr {
    Expr::sort(Level::zero())
  }

  fn mk_cv(name: &str) -> ConstantVal {
    ConstantVal { name: n(name), level_params: vec![], typ: sort0() }
  }

  #[test]
  fn empty_env() {
    let env = Env::default();