Enum Kind

#[repr(u16)]
pub enum Kind {
    UnsafeBlock = 0,
    Unimplemented {
        issue_id: Option<u32>,
        details: Option<String>,
    },
    AssertionFailure {
        details: String,
    },
    UnallowedMutRef = 3,
    UnsupportedMacro {
        id: String,
    },
    ErrorParsingMacroInvocation {
        macro_id: String,
        details: String,
    },
    ClosureMutatesParentBindings {
        bindings: Vec<String>,
    },
    ArbitraryLHS = 7,
    ExplicitRejection {
        reason: String,
    },
    UnsupportedTupleSize {
        tuple_size: u32,
        reason: String,
    },
    ExpectedMutRef = 10,
    NonTrivialAndMutFnInput = 11,
    AttributeRejected {
        reason: String,
    },
    FStarParseError {
        fstar_snippet: String,
        details: String,
    },
}

Variants

UnsafeBlock = 0

Unsafe code is not supported

Unimplemented

A feature is not currently implemented, but

Fields

issue_id: Option<u32>

Issue on the GitHub repository

details: Option<String>

AssertionFailure

Unknown error

Fields

details: String

UnallowedMutRef = 3

Unallowed mutable reference

UnsupportedMacro

Unsupported macro invokation

Fields

id: String

ErrorParsingMacroInvocation

Error parsing a macro invocation to a macro treated specifcially by a backend

Fields

macro_id: String

details: String

ClosureMutatesParentBindings

Mutation of bindings living outside a closure scope are not supported

Fields

bindings: Vec<String>

ArbitraryLHS = 7

Assignation of an arbitrary left-hand side is not supported. lhs = e is fine only when lhs is a combination of local identifiers, field accessors and index accessors.

ExplicitRejection

A phase explicitely rejected this chunk of code

Fields

reason: String

UnsupportedTupleSize

A backend doesn’t support a tuple size

Fields

tuple_size: u32

reason: String

ExpectedMutRef = 10

NonTrivialAndMutFnInput = 11

&mut inputs should be trivial patterns

AttributeRejected

An hax attribute (from hax-lib-macros) was rejected

Fields

reason: String

FStarParseError

A snippet of F* code could not be parsed

Fields

fstar_snippet: String

details: String

Implementations

impl Kind

pub fn discriminant(&self) -> u16

pub fn code(&self) -> String

Trait Implementations

impl Clone for Kind

fn clone(&self) -> Kind

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Kind

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for Kind

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl JsonSchema for Kind

fn schema_name() -> String

The name of the generated JSON Schema.

fn schema_id() -> Cow<'static, str>

Returns a string that uniquely identifies the schema produced by this type.

fn json_schema(gen: &mut SchemaGenerator) -> Schema

Generates a JSON Schema for this type.

fn is_referenceable() -> bool

Whether JSON Schemas generated for this type should be re-used where possible using the $ref keyword.

impl Serialize for Kind

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.