Enum Type 

pub enum Type {
    Nat,
    Int,
    Bool,
    String,
    Unit,
    Float,
    Fixed {
        bits: u32,
        signed: bool,
    },
    Data {
        name: String,
    },
    Array {
        element: Box<Self>,
    },
    Named {
        path: Vec<String>,
        span: Option<Span>,
    },
    Literal,
    Hypothesis,
    Output,
}

A portable-core type, or a surface type reference before resolution.

Variants

Nat

Int

Bool

String

Unit

Float

A JavaScript Number: an IEEE-754 binary64.

Fixed

Fields

bits: u32

signed: bool

Data

A resolved data type, named by its qualified path.

Fields

name: String

Array

A JavaScript array, which the portable core reads and never mutates.

Fields

element: Box<Self>

Named

A surface reference to a declared type, resolved by the checker.

Fields

path: Vec<String>

span: Option<Span>

Literal

The type of a numeral whose type the context has not fixed yet.

Hypothesis

A proof hypothesis bound by a case split (proof plans only).

Output

The lines a program has printed, newest first: only the targets whose programs are pure carry them, as a value (see output).

Implementations

impl Type

pub fn key(&self) -> String

The type’s identity: nat, i32, data:Tree.

pub const fn kind(&self) -> &'static str

The kind discriminant as the JavaScript runtime spells it.

pub fn same(&self, other: &Self) -> bool

pub const fn is_numeric(&self) -> bool

pub const fn is_float(&self) -> bool

pub const fn is_ordered(&self) -> bool

True for the types < orders: the integers and Numbers.

pub const fn is_natural(&self) -> bool

True when every value of the type is a non-negative integer.

pub const fn is_literal(&self) -> bool

pub fn element(&self) -> Option<&Self>

The element type of an array.

pub fn data_name(&self) -> Option<&str>

The data type’s qualified name.

Trait Implementations

impl Clone for Type

fn clone(&self) -> Type

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Type

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for Type

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

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Eq for Type

impl PartialEq for Type

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

Equality operator ==.

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

Inequality operator !=.

impl Serialize for Type

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

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for Type