Enum InductiveError 

pub enum InductiveError {
    AlreadyDefined(Name),
    UndefinedType(Name),
    InvalidConstructorType(Name),
    UniverseTooSmall(String),
    NonStrictlyPositive(Name),
    Other(String),
}

Errors that can occur when checking an inductive type definition.

Variants

AlreadyDefined(Name)

The type name is already defined.

UndefinedType(Name)

A constructor references a type that is not in scope.

InvalidConstructorType(Name)

A constructor has an invalid type (not a Pi ending in the inductive type).

UniverseTooSmall(String)

The universe level is not large enough.

NonStrictlyPositive(Name)

A non-strictly positive occurrence of the type.

Other(String)

General error.

Trait Implementations

impl Clone for InductiveError

fn clone(&self) -> InductiveError

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for InductiveError

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

Formats the value using the given formatter.

impl Display for InductiveError

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

Formats the value using the given formatter.

impl PartialEq for InductiveError

fn eq(&self, other: &InductiveError) -> 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 StructuralPartialEq for InductiveError