mathlib documentation

core / init.meta.feature_search

structure feature_search.feature_cfg  :
Type
  • ignore_tc : bool
  • ignore_pi_domain : bool
  • ignore_type_args : bool
  • ignore_decidable : bool
  • ignore_conns : bool
Instances for feature_search.feature_cfg
  • feature_search.feature_cfg.has_sizeof_inst
meta constant feature_search.predictor  :
Type
inductive feature_search.predictor_type  :
Type
Instances for feature_search.predictor_type
  • feature_search.predictor_type.has_sizeof_inst
structure feature_search.predictor_cfg  :
Type
Instances for feature_search.predictor_cfg
  • feature_search.predictor_cfg.has_sizeof_inst