Skip to main content

ConstGenericDbVar

Type Alias ConstGenericDbVar 

Source
pub type ConstGenericDbVar = DeBruijnVar<ConstGenericVarId>;

Aliased Type§

pub enum ConstGenericDbVar {
    Bound(DeBruijnId, ConstGenericVarId),
    Free(ConstGenericVarId),
}

Variants§

§

Bound(DeBruijnId, ConstGenericVarId)

A variable attached to the nth binder, counting from the innermost.

§

Free(ConstGenericVarId)

A variable not attached to a particular binder. Can be used for various purposes which manipulating types, e.g. as inference variables or placeholders. If --unbind-item-vars is set, we use Free variables to refer to the item binders; Free variables should not otherwise be found in the output of running charon.

Trait Implementations§

Source§

impl<C: AstFormatter> FmtWithCtx<C> for ConstGenericDbVar

Source§

fn fmt_with_ctx(&self, ctx: &C, f: &mut Formatter<'_>) -> Result

Source§

fn with_ctx<'a>(&'a self, ctx: &'a C) -> WithCtx<'a, C, Self>

Returns a struct that implements Display. This allows the following: Read more
Source§

fn to_string_with_ctx(&self, ctx: &C) -> String

Source§

impl TryFrom<ConstantExprKind> for ConstGenericDbVar

Source§

type Error = ()

The type returned in the event of a conversion error.
Source§

fn try_from(e: ConstantExprKind) -> Result<Self, Self::Error>

Performs the conversion.