normalize_alias_reft

Function normalize_alias_reft 

Source
fn normalize_alias_reft<'tcx>(
    genv: GlobalEnv<'_, 'tcx>,
    def_id: DefId,
    infcx: &InferCtxt<'tcx>,
    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.