Enum TypeExpr 

pub enum TypeExpr {
    Hole,
    NamedHole(String),
    Ident(String),
    NatLit(String),
    Literal(String),
    App(Box<TypeExpr>, Box<TypeExpr>),
    BinOp {
        op: String,
        left: Box<TypeExpr>,
        right: Box<TypeExpr>,
    },
    UnaryOp {
        op: String,
        arg: Box<TypeExpr>,
    },
    Postfix {
        arg: Box<TypeExpr>,
        op: String,
    },
    Arrow(Box<TypeExpr>, Box<TypeExpr>),
    Forall {
        binders: Vec<Binder>,
        body: Box<TypeExpr>,
    },
    Exists {
        binders: Vec<Binder>,
        body: Box<TypeExpr>,
    },
    Lambda {
        binders: Vec<Binder>,
        body: Box<TypeExpr>,
    },
    Pi {
        binder: Binder,
        body: Box<TypeExpr>,
    },
    Proj {
        base: Box<TypeExpr>,
        field: String,
    },
    Sort {
        name: String,
        level: Option<Box<TypeExpr>>,
    },
    Raw(String),
}

Surface type expression used for indexing and pattern matching.

Variants

Hole

Anonymous hole _ (search only, or explicit underscore in source).

NamedHole(String)

Named hole ?a (search patterns; also metavariable-like tokens).

Ident(String)

Identifier / constant, e.g. Nat, List, add_comm.

NatLit(String)

Numeric literal.

Literal(String)

String / char literal (kept raw).

App(Box<TypeExpr>, Box<TypeExpr>)

Function application f a (left-associative chain folded as nested apps).

BinOp

Infix binary operator: a + b, x = y, P ∧ Q, etc.

Fields

op: String

left: Box<TypeExpr>

right: Box<TypeExpr>

UnaryOp

Unary prefix operator: ¬P, -n, ⁻¹ is usually postfix — see Postfix.

Fields

op: String

arg: Box<TypeExpr>

Postfix

Postfix operator: a⁻¹, f'.

Fields

arg: Box<TypeExpr>

op: String

Arrow(Box<TypeExpr>, Box<TypeExpr>)

A → B / A -> B

Forall

∀ binders, body / forall

Fields

binders: Vec<Binder>

body: Box<TypeExpr>

Exists

∃ binders, body / exists

Fields

binders: Vec<Binder>

body: Box<TypeExpr>

Lambda

fun binders => body / λ

Fields

binders: Vec<Binder>

body: Box<TypeExpr>

Pi

Explicit binder-typed term used in Pi: (x : A) → B

Fields

binder: Binder

body: Box<TypeExpr>

Proj

Projection e.field / e.1

Fields

base: Box<TypeExpr>

field: String

Sort

Universe / sort: Prop, Type, Type u, Sort u, Type*, Sort _

Fields

name: String

level: Option<Box<TypeExpr>>

Raw(String)

Explicit list / structure sugar kept as raw for robustness.

Implementations

impl TypeExpr

pub fn apps(f: TypeExpr, args: impl IntoIterator<Item = TypeExpr>) -> TypeExpr

Fold a function and argument list into nested App nodes.

pub fn idents(&self) -> Vec<&str>

Collect free identifiers (rough; for indexing).

pub fn operators(&self) -> Vec<&str>

Operators appearing in the expression (for inverted index).

pub fn conclusion(&self) -> &TypeExpr

Strip outer binders / arrows to obtain the main conclusion.

∀ x, P → Q → R concludes with R.

pub fn head_key(&self) -> String

Head symbol for inverted indexing (operator or leading ident).

pub fn surface(&self) -> String

Pretty-print a compact surface form (for display / cache).

Trait Implementations

impl Clone for TypeExpr

fn clone(&self) -> TypeExpr

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for TypeExpr

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for TypeExpr

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

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Eq for TypeExpr

impl PartialEq for TypeExpr

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

Equality operator ==.

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

Inequality operator !=.

impl Serialize for TypeExpr

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 TypeExpr