Enum SurfaceExpr 

pub enum SurfaceExpr {
    Sort(SortKind),
    Var(String),
    App(Box<Located<SurfaceExpr>>, Box<Located<SurfaceExpr>>),
    Lam(Vec<Binder>, Box<Located<SurfaceExpr>>),
    Pi(Vec<Binder>, Box<Located<SurfaceExpr>>),
    Let(String, Option<Box<Located<SurfaceExpr>>>, Box<Located<SurfaceExpr>>, Box<Located<SurfaceExpr>>),
    Lit(Literal),
    Ann(Box<Located<SurfaceExpr>>, Box<Located<SurfaceExpr>>),
    Hole,
    Proj(Box<Located<SurfaceExpr>>, String),
    If(Box<Located<SurfaceExpr>>, Box<Located<SurfaceExpr>>, Box<Located<SurfaceExpr>>),
    Match(Box<Located<SurfaceExpr>>, Vec<MatchArm>),
    Do(Vec<DoAction>),
    Have(String, Box<Located<SurfaceExpr>>, Box<Located<SurfaceExpr>>, Box<Located<SurfaceExpr>>),
    Suffices(String, Box<Located<SurfaceExpr>>, Box<Located<SurfaceExpr>>),
    Show(Box<Located<SurfaceExpr>>, Box<Located<SurfaceExpr>>),
    NamedArg(Box<Located<SurfaceExpr>>, String, Box<Located<SurfaceExpr>>),
    AnonymousCtor(Vec<Located<SurfaceExpr>>),
    ListLit(Vec<Located<SurfaceExpr>>),
    Tuple(Vec<Located<SurfaceExpr>>),
    Return(Box<Located<SurfaceExpr>>),
    StringInterp(Vec<StringPart>),
    Range(Option<Box<Located<SurfaceExpr>>>, Option<Box<Located<SurfaceExpr>>>),
    ByTactic(Vec<Located<TacticRef>>),
    Calc(Vec<CalcStep>),
}

Surface-level expression (before elaboration).

Variants

Sort(SortKind)

Sort: Type, Prop, Type u, Sort u

Var(String)

Variable reference

App(Box<Located<SurfaceExpr>>, Box<Located<SurfaceExpr>>)

Application: f a

Lam(Vec<Binder>, Box<Located<SurfaceExpr>>)

Lambda: fun (x : alpha) => body or lambda (x : alpha), body

Pi(Vec<Binder>, Box<Located<SurfaceExpr>>)

Pi type: forall (x : alpha), beta or (x : alpha) -> beta

Let(String, Option<Box<Located<SurfaceExpr>>>, Box<Located<SurfaceExpr>>, Box<Located<SurfaceExpr>>)

Let binding: let x : alpha := v in body

Lit(Literal)

Literal value

Ann(Box<Located<SurfaceExpr>>, Box<Located<SurfaceExpr>>)

Explicit type annotation: (e : tau)

Hole

Placeholder: _

Proj(Box<Located<SurfaceExpr>>, String)

Projection: e.n

If(Box<Located<SurfaceExpr>>, Box<Located<SurfaceExpr>>, Box<Located<SurfaceExpr>>)

If-then-else: if c then t else e

Match(Box<Located<SurfaceExpr>>, Vec<MatchArm>)

Match expression: match e with | pat => rhs | …

Do(Vec<DoAction>)

Do notation: do { … }

Have(String, Box<Located<SurfaceExpr>>, Box<Located<SurfaceExpr>>, Box<Located<SurfaceExpr>>)

Have expression: have h : T := proof; body

Suffices(String, Box<Located<SurfaceExpr>>, Box<Located<SurfaceExpr>>)

Suffices expression: suffices h : T by tactic; body

Show(Box<Located<SurfaceExpr>>, Box<Located<SurfaceExpr>>)

Show expression: show T from expr

NamedArg(Box<Located<SurfaceExpr>>, String, Box<Located<SurfaceExpr>>)

Named argument application: f (x := e)

AnonymousCtor(Vec<Located<SurfaceExpr>>)

Anonymous constructor: (langle) a, b, c (rangle)

ListLit(Vec<Located<SurfaceExpr>>)

List literal: [1, 2, 3]

Tuple(Vec<Located<SurfaceExpr>>)

Tuple: (a, b) or (a, b, c)

Return(Box<Located<SurfaceExpr>>)

Return expression (used in do notation): return e

StringInterp(Vec<StringPart>)

String interpolation: s!"hello {name}"

Range(Option<Box<Located<SurfaceExpr>>>, Option<Box<Located<SurfaceExpr>>>)

Range expression: a..b, ..b, a..

ByTactic(Vec<Located<TacticRef>>)

By-tactic expression: by tactic1; tactic2; ...

Calc(Vec<CalcStep>)

Calc expression: calculational proof

Implementations

impl SurfaceExpr

pub fn var(name: &str) -> Self

Create a variable expression.

pub fn nat(n: u64) -> Self

Create a natural number literal expression.

pub fn string(s: &str) -> Self

Create a string literal expression.

pub fn float(v: f64) -> Self

Create a float literal expression.

pub fn is_hole(&self) -> bool

Check if this expression is a hole/placeholder.

pub fn is_var(&self) -> bool

Check if this expression is a variable.

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

Get the variable name if this is a variable.

Trait Implementations

impl Clone for SurfaceExpr

fn clone(&self) -> SurfaceExpr

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SurfaceExpr

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

Formats the value using the given formatter.

impl Display for SurfaceExpr

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

Formats the value using the given formatter.

impl PartialEq for SurfaceExpr

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