Enum IdrisType 

pub enum IdrisType {
    Type,
    Integer,
    Nat,
    Bool,
    String,
    Char,
    Double,
    List(Box<IdrisType>),
    Vect(Box<IdrisExpr>, Box<IdrisType>),
    Pair(Box<IdrisType>, Box<IdrisType>),
    Unit,
    Function(Box<IdrisType>, Box<IdrisType>),
    Linear(Box<IdrisType>, Box<IdrisType>),
    Erased(Box<IdrisType>, Box<IdrisType>),
    Pi(String, Box<IdrisType>, Box<IdrisType>),
    Data(String, Vec<IdrisType>),
    Interface(String, Vec<IdrisType>),
    Var(String),
    IO(Box<IdrisType>),
    Maybe(Box<IdrisType>),
    Either(Box<IdrisType>, Box<IdrisType>),
}

A type in Idris 2’s type theory.

Variants

Type

Type — the type of types (universe).

Integer

Integer — arbitrary-precision integer.

Nat

Nat — natural number.

Bool

Bool — boolean.

String

String — text string.

Char

Char — unicode character.

Double

Double — 64-bit floating-point.

List(Box<IdrisType>)

List a — list type.

Vect(Box<IdrisExpr>, Box<IdrisType>)

Vect n a — length-indexed vector.

Pair(Box<IdrisType>, Box<IdrisType>)

(a, b) — pair / product type.

Unit

() / Unit — unit type.

Function(Box<IdrisType>, Box<IdrisType>)

a -> b — function type (unrestricted arrow).

Linear(Box<IdrisType>, Box<IdrisType>)

(1 x : a) -> b — linear function type.

Erased(Box<IdrisType>, Box<IdrisType>)

(0 x : a) -> b — erased argument function.

Pi(String, Box<IdrisType>, Box<IdrisType>)

(x : a) -> b x — dependent function type (Pi).

Data(String, Vec<IdrisType>)

A named data type reference, e.g. MyType, Maybe Int.

Interface(String, Vec<IdrisType>)

An interface constraint, e.g. Eq a => ...

Var(String)

A type variable (used in polymorphic types).

IO(Box<IdrisType>)

IO a — IO action type.

Maybe(Box<IdrisType>)

Maybe a — optional type.

Either(Box<IdrisType>, Box<IdrisType>)

Either a b — sum type.

Trait Implementations

impl Clone for IdrisType

fn clone(&self) -> IdrisType

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for IdrisType

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

Formats the value using the given formatter.

impl Display for IdrisType

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

Formats the value using the given formatter.

impl PartialEq for IdrisType

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