mathlib documentation

core / init.meta.feature_search

source
structure feature_search.feature_cfg  :
Type
  • ignore_tc : bool
  • ignore_pi_domain : bool
  • ignore_type_args : bool
  • ignore_decidable : bool
  • ignore_conns : bool
source
@[protected, instance]
meta def feature_search.feature.decidable_eq  :
decidable_eq feature_search.feature
source
meta inductive feature_search.feature  :
Type
source
@[protected]
meta def feature_search.feature.to_string  :
feature_search.feature → string
source
@[protected]
meta def feature_search.feature.repr  :
feature_search.feature → string
source
@[protected, instance]
meta def feature_search.feature.has_to_string  :
has_to_string feature_search.feature
source
@[protected, instance]
meta def feature_search.feature.has_repr  :
has_repr feature_search.feature
source
@[protected, instance]
meta def feature_search.feature.has_to_tactic_format  :
has_to_tactic_format feature_search.feature
source
@[protected, instance]
meta def feature_search.feature.has_to_format  :
has_to_format feature_search.feature
source
meta constant feature_search.feature_vec  :
Type
source
meta constant feature_search.feature_vec.of_expr (env : environment) (e : expr) (cfg : feature_search.feature_cfg := {ignore_tc := tt, ignore_pi_domain := tt, ignore_type_args := tt, ignore_decidable := tt, ignore_conns := tt}) :
feature_search.feature_vec
source
meta constant feature_search.feature_vec.of_exprs (env : environment) (es : list expr) (cfg : feature_search.feature_cfg := {ignore_tc := tt, ignore_pi_domain := tt, ignore_type_args := tt, ignore_decidable := tt, ignore_conns := tt}) :
list feature_search.feature_vec
source
@[protected]
meta constant feature_search.feature_vec.union (a b : feature_search.feature_vec) :
feature_search.feature_vec
source
@[protected, instance]
meta def feature_search.feature_vec.has_union  :
has_union feature_search.feature_vec
source
@[protected]
meta constant feature_search.feature_vec.isect (a b : feature_search.feature_vec) :
feature_search.feature_vec
source
@[protected, instance]
meta def feature_search.feature_vec.has_inter  :
has_inter feature_search.feature_vec
source
meta def feature_search.feature_vec.of_proof (prf : expr) (cfg : feature_search.feature_cfg := {ignore_tc := tt, ignore_pi_domain := tt, ignore_type_args := tt, ignore_decidable := tt, ignore_conns := tt}) :
tactic feature_search.feature_vec
source
meta def feature_search.feature_vec.of_thm (n : name) (cfg : feature_search.feature_cfg := {ignore_tc := tt, ignore_pi_domain := tt, ignore_type_args := tt, ignore_decidable := tt, ignore_conns := tt}) :
tactic feature_search.feature_vec
source
@[protected]
meta constant feature_search.feature_vec.to_list (fv : feature_search.feature_vec) :
list feature_search.feature
source
@[protected, instance]
meta def feature_search.feature_vec.has_to_string  :
has_to_string feature_search.feature_vec
source
@[protected, instance]
meta def feature_search.feature_vec.has_repr  :
has_repr feature_search.feature_vec
source
@[protected, instance]
meta def feature_search.feature_vec.has_to_tactic_format  :
has_to_tactic_format feature_search.feature_vec
source
@[protected, instance]
meta def feature_search.feature_vec.has_to_format  :
has_to_format feature_search.feature_vec
source
meta constant feature_search.feature_stats  :
Type
source
meta constant feature_search.feature_stats.of_feature_vecs (fvs : list feature_search.feature_vec) :
feature_search.feature_stats
source
meta constant feature_search.feature_stats.idf (fs : feature_search.feature_stats) (f : feature_search.feature) :
native.float
source
meta constant feature_search.feature_stats.norm (fs : feature_search.feature_stats) (fv : feature_search.feature_vec) :
native.float
source
meta constant feature_search.feature_stats.dotp (fs : feature_search.feature_stats) (fv1 fv2 : feature_search.feature_vec) :
native.float
source
meta constant feature_search.feature_stats.cosine_similarity (fs : feature_search.feature_stats) (fv1 fv2 : feature_search.feature_vec) :
native.float
source
meta constant feature_search.feature_stats.features (fs : feature_search.feature_stats) :
list feature_search.feature
source
meta def feature_search.feature_stats.features_with_idf (fs : feature_search.feature_stats) :
list (feature_search.feature × native.float)
source
@[protected, instance]
meta def feature_search.feature_stats.has_to_string  :
has_to_string feature_search.feature_stats
source
@[protected, instance]
meta def feature_search.feature_stats.has_repr  :
has_repr feature_search.feature_stats
source
@[protected, instance]
meta def feature_search.feature_stats.has_to_tactic_format  :
has_to_tactic_format feature_search.feature_stats
source
@[protected, instance]
meta def feature_search.feature_stats.has_to_format  :
has_to_format feature_search.feature_stats
source
meta constant feature_search.predictor  :
Type
source
meta constant feature_search.predictor.predict (p : feature_search.predictor) (goal : feature_search.feature_vec) (max_results : ℕ) :
list (name × native.float)
source
@[protected, instance]
def feature_search.predictor_type.decidable_eq  :
decidable_eq feature_search.predictor_type
source
inductive feature_search.predictor_type  :
Type
source
structure feature_search.predictor_cfg  :
Type
source
meta constant environment.mk_predictor (env : environment) (cfg : feature_search.predictor_cfg := {to_feature_cfg := {ignore_tc := tt, ignore_pi_domain := tt, ignore_type_args := tt, ignore_decidable := tt, ignore_conns := tt}, type := feature_search.predictor_type.bayes}) :
feature_search.predictor