Type Alias FluxDefId

pub type FluxDefId = FluxId<DefId>;

Aliased Type

struct FluxDefId {
    parent: DefId,
    name: Symbol,
}

Fields

parent: DefId

name: Symbol

Implementations

impl FluxDefId

pub fn as_local(self) -> Option<FluxLocalDefId>

pub fn expect_local(self) -> FluxLocalDefId

pub fn krate(self) -> CrateNum

pub fn index(self) -> FluxId<DefIndex>

Trait Implementations

impl Pretty for FluxDefId

fn fmt(&self, cx: &PrettyCx<'_, '_>, f: &mut Formatter<'_>) -> Result

fn default_cx(tcx: TyCtxt<'_>) -> PrettyCx<'_, '_>

impl SliceInternable for FluxDefId

fn storage() -> &'static InternStorage<[Self]>

impl TypeFoldable for FluxDefId

fn try_fold_with<F: FallibleTypeFolder>( &self, _: &mut F, ) -> Result<Self, F::Error>

fn fold_with<F: TypeFolder>(&self, _: &mut F) -> Self

fn normalize(&self, genv: GlobalEnv<'_, '_>) -> Self

Normalize expressions by applying beta reductions for tuples and lambda abstractions.

fn replace_holes( &self, f: impl FnMut(&[BoundVariableKinds], HoleKind) -> Expr, ) -> Self

Replaces all holes with the result of calling a closure. The closure takes a list with all the layers of bound variables at the point the hole was found. Each layer corresponds to the list of bound variables at that level. The list is ordered from outermost to innermost binder, i.e., the last element is the binder closest to the hole.

fn with_holes(&self) -> Self

Remove all refinements and turn each underlying BaseTy into a TyKind::Exists with a TyKind::Constr and a hole. For example, Vec<{v. i32[v] | v > 0}>[n] becomes {n. Vec<{v. i32[v] | *}>[n] | *}.

fn replace_evars( &self, f: &mut impl FnMut(EVid) -> Option<Expr>, ) -> Result<Self, EVid>

fn shift_in_escaping(&self, amount: u32) -> Self

fn shift_out_escaping(&self, amount: u32) -> Self

fn erase_regions(&self) -> Self

impl TypeVisitable for FluxDefId

fn visit_with<V: TypeVisitor>(&self, _: &mut V) -> ControlFlow<V::BreakTy>

fn has_escaping_bvars(&self) -> bool

fn has_escaping_bvars_at_or_above(&self, binder: DebruijnIndex) -> bool

Returns true if self has any late-bound vars that are either bound by binder or bound by some binder outside of binder. If binder is ty::INNERMOST, this indicates whether there are any late-bound vars that appear free.

fn fvars(&self) -> FxHashSet<Name>

Returns the set of all free variables. For example, Vec<i32[n]>{v : v > m} returns {n, m}.