normalize_alias_reft

flux_infer::projections

Function normalize_alias_reft 

Source 
fn normalize_alias_reft(
    genv: GlobalEnv<'_, '_>,
    def_id: DefId,
    infcx: &InferCtxt<'_>,
    alias_reft: &AliasReft,
    refine_args: &RefineArgs,
) -> QueryResult<(bool, Expr)>
Expand description

Normalizes an AliasReft. This uses the trait solver to find the ImplSourceUserDefinedData and uses the args there, which we map back to Flux via refining. This loses refinements, but that’s fine because AliasReft should not rely on refinements for trait solving.