Enum CoqTerm 

pub enum CoqTerm {
    Var(String),
    App(Box<CoqTerm>, Vec<CoqTerm>),
    Lambda(Vec<(String, CoqTerm)>, Box<CoqTerm>),
    Forall(Vec<(String, CoqTerm)>, Box<CoqTerm>),
    Prod(Box<CoqTerm>, Box<CoqTerm>),
    Let(String, Option<Box<CoqTerm>>, Box<CoqTerm>, Box<CoqTerm>),
    Match(Box<CoqTerm>, Option<String>, Vec<CoqBranch>),
    Fix(Vec<CoqFixPoint>),
    Sort(CoqSort),
    Hole,
    Num(i64),
    Str(String),
    Cast(Box<CoqTerm>, Box<CoqTerm>),
    Explicit(Box<CoqTerm>),
    Tuple(Vec<CoqTerm>),
    List(Vec<CoqTerm>),
    IfThenElse(Box<CoqTerm>, Box<CoqTerm>, Box<CoqTerm>),
}

Gallina term AST.

Variants

Var(String)

Variable or qualified name: nat, List.length, Nat.add

App(Box<CoqTerm>, Vec<CoqTerm>)

Application: f a b c

Lambda(Vec<(String, CoqTerm)>, Box<CoqTerm>)

Lambda abstraction: fun (x : T) (y : U) => body

Forall(Vec<(String, CoqTerm)>, Box<CoqTerm>)

Universal quantifier: forall (x : T), P x

Prod(Box<CoqTerm>, Box<CoqTerm>)

Non-dependent function type: T -> U

Let(String, Option<Box<CoqTerm>>, Box<CoqTerm>, Box<CoqTerm>)

Let binding: let x [: T] := rhs in body

Match(Box<CoqTerm>, Option<String>, Vec<CoqBranch>)

Pattern match: match scrutinee [as name] with | ... end

Fix(Vec<CoqFixPoint>)

(Mutual) fixpoint: fix f (n : nat) ... := body

Sort(CoqSort)

Universe sort: Prop, Set, Type

Hole

Hole / unification variable: _

Num(i64)

Integer literal: 0, 42, -1

Str(String)

String literal: "hello"

Cast(Box<CoqTerm>, Box<CoqTerm>)

Coercion / type ascription: (term : T)

Explicit(Box<CoqTerm>)

Implicit argument: @f (explicit application)

Tuple(Vec<CoqTerm>)

Tuple/pair: (a, b) (syntactic sugar for pair a b)

List(Vec<CoqTerm>)

List literal: [a; b; c]

IfThenElse(Box<CoqTerm>, Box<CoqTerm>, Box<CoqTerm>)

If-then-else: if b then t else f

Implementations

impl CoqTerm

pub fn emit(&self, indent: usize) -> String

Emit as a Gallina string with the given indentation.

Trait Implementations

impl Clone for CoqTerm

fn clone(&self) -> CoqTerm

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CoqTerm

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

Formats the value using the given formatter.

impl PartialEq for CoqTerm

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