Enum TyKind

pub enum TyKind {
    Base(BaseTy),
    Indexed {
        bty: BaseTy,
        indices: Indices,
    },
    Exists {
        bind: Ident,
        bty: BaseTy,
        pred: Expr,
    },
    GeneralExists {
        params: RefineParams,
        ty: Box<Ty>,
        pred: Option<Expr>,
    },
    Ref(Mutability, Box<Ty>),
    Constr(Expr, Box<Ty>),
    Tuple(Vec<Ty>),
    Array(Box<Ty>, ConstArg),
    ImplTrait(NodeId, GenericBounds),
    Hole,
}

Variants

Base(BaseTy)

ty

Indexed

B[r]

Fields

bty: BaseTy

indices: Indices

Exists

B{v: r}

Fields

bind: Ident

bty: BaseTy

pred: Expr

GeneralExists

Fields

params: RefineParams

ty: Box<Ty>

pred: Option<Expr>

Ref(Mutability, Box<Ty>)

Mutable or shared reference

Constr(Expr, Box<Ty>)

Constrained type: an exists without binder

Tuple(Vec<Ty>)

Array(Box<Ty>, ConstArg)

ImplTrait(NodeId, GenericBounds)

The NodeId is used to resolve the type to a corresponding OpaqueTy

Hole

Trait Implementations

impl Debug for TyKind

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

Formats the value using the given formatter.