Enum StructureRefusal 

pub enum StructureRefusal {
    NotAnInductive {
        inductive: String,
    },
    AlreadyAStructure {
        inductive: String,
    },
    Sealed {
        inductive: String,
    },
    NotStructureShaped {
        inductive: String,
        constructors: usize,
        indices: usize,
    },
    ShortConstructor {
        constructor: String,
        params: usize,
    },
    Recursive {
        inductive: String,
    },
    ProjectionCount {
        inductive: String,
        fields: usize,
        projections: usize,
    },
    NotADefinition {
        projection: String,
    },
    UniverseArity {
        projection: String,
        inductive: String,
        expected: usize,
        found: usize,
    },
    DoesNotCompute {
        projection: String,
        field: usize,
        inductive: String,
    },
    WrongFieldType {
        projection: String,
        field: usize,
        inductive: String,
    },
}

Why structure η was refused. Every variant names the first condition that failed.

Variants

NotAnInductive

The named inductive is not declared.

Fields

inductive: String

AlreadyAStructure

The inductive already has structure η.

Fields

inductive: String

Sealed

A native nested positivity check depends on the inductive, so it cannot change.

Fields

inductive: String

NotStructureShaped

A structure has exactly one constructor and no indices.

Fields

inductive: String

constructors: usize

indices: usize

ShortConstructor

The constructor’s type binds fewer binders than the inductive has parameters.

Fields

constructor: String

params: usize

Recursive

The inductive’s mutual block is recursive.

Fields

inductive: String

ProjectionCount

The number of projections differs from the number of fields.

Fields

inductive: String

fields: usize

projections: usize

NotADefinition

A projection is not a transparent definition.

Fields

projection: String

UniverseArity

A projection’s universe telescope is not the inductive’s.

Fields

projection: String

inductive: String

expected: usize

found: usize

DoesNotCompute

projᵢ p̄ (mk p̄ f̄) is not definitionally fᵢ.

Fields

projection: String

field: usize

inductive: String

WrongFieldType

projᵢ p̄ (mk p̄ f̄) computes fᵢ but is ill typed, or not of the field’s type.

Fields

projection: String

field: usize

inductive: String

Trait Implementations

impl Clone for StructureRefusal

fn clone(&self) -> StructureRefusal

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for StructureRefusal

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

Formats the value using the given formatter.

impl Display for StructureRefusal

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

Formats the value using the given formatter.

impl Error for StructureRefusal

fn source(&self) -> Option<&(dyn Error + 'static)>

Returns the lower-level source of this error, if any.

fn description(&self) -> &str

👎Deprecated since 1.42.0:

use the Display impl or to_string()

fn cause(&self) -> Option<&dyn Error>

👎Deprecated since 1.33.0:

replaced by Error::source, which can support downcasting

fn provide<'a>(&'a self, request: &mut Request<'a>)

🔬This is a nightly-only experimental API. (error_generic_member_access)

Provides type-based access to context intended for error reports.

impl PartialEq for StructureRefusal

fn eq(&self, other: &StructureRefusal) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for StructureRefusal

impl StructuralPartialEq for StructureRefusal