Crate flux_fhir_analysis 

Modules

conv 🔒

Conversion from types in fhir to types in rty

errors 🔒

wf 🔒

Checks type well-formedness

Structs

OpaqueTyParamCollector 🔒

Collects the refinement params mentioned in the bounds of opaque types.

ParamCollector 🔒

Collects all refinement params mentioned in the visited nodes.

Functions

adt_def 🔒

adt_sort_def_of 🔒

assoc_refinement_body 🔒

assoc_refinements_of 🔒

check_wf 🔒

conjoin_bind_exprs 🔒

constant_info 🔒

default_assoc_refinement_body 🔒

flux_def_ident_span 🔒

fn_sig 🔒

func_sort 🔒

generics_of 🔒

invariants_of 🔒

Errors are reported at the definition of the adt. If the invariants fail to convert, we continue as if the adt had no invariants. This is sound because the invariants are then neither checked (when constructing the adt) nor assumed (when using it).

item_bounds 🔒

late_bound_refinement_params 🔒

See GlobalEnv::late_bound_refinement_params

normalized_defns 🔒

predicates_of 🔒

prim_rel 🔒

primop_props 🔒

provide

qualifiers 🔒

refinement_generics_of 🔒

sort_decl_param_count 🔒

sort_of_assoc_reft 🔒

static_info 🔒

try_invariants_of 🔒

try_normalized_defns 🔒

ty_param_owner 🔒

type_of 🔒

variants_of 🔒