Enum WellFormedResult 

pub enum WellFormedResult {
    Ok,
    TypeNotSort {
        description: String,
    },
    TypeMismatch {
        description: String,
    },
    FreeVariables {
        vars: Vec<String>,
    },
    DuplicateName {
        name: String,
    },
    UniverseError {
        description: String,
    },
}

Well-formedness checking result for a declaration.

Variants

Ok

The declaration is well-formed.

TypeNotSort

The declaration has a type that is not a sort.

Fields

description: String

Description of the type-is-not-a-sort error.

TypeMismatch

The value does not have the declared type.

Fields

description: String

Description of the type mismatch.

FreeVariables

The declaration contains free variables.

Fields

vars: Vec<String>

Names of the free variables found.

DuplicateName

The name is already declared.

Fields

name: String

The duplicate name.

UniverseError

Universe level inconsistency.

Fields

description: String

Description of the universe error.

Implementations

impl WellFormedResult

pub fn is_ok(&self) -> bool

Returns true if the result indicates a well-formed declaration.

pub fn description(&self) -> String

Returns a human-readable description of the result.

Trait Implementations

impl Clone for WellFormedResult

fn clone(&self) -> WellFormedResult

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for WellFormedResult

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

Formats the value using the given formatter.

impl PartialEq for WellFormedResult

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

impl StructuralPartialEq for WellFormedResult