Enum Declaration 

pub enum Declaration {
    Axiom {
        name: Name,
        univ_params: Vec<Name>,
        ty: Expr,
    },
    Definition {
        name: Name,
        univ_params: Vec<Name>,
        ty: Expr,
        val: Expr,
        hint: ReducibilityHint,
    },
    Theorem {
        name: Name,
        univ_params: Vec<Name>,
        ty: Expr,
        val: Expr,
    },
    Opaque {
        name: Name,
        univ_params: Vec<Name>,
        ty: Expr,
        val: Expr,
    },
}

A declaration in the global environment (legacy format).

Variants

Axiom

Axiom: postulated type without proof

Fields

name: Name

Name of the axiom

univ_params: Vec<Name>

Universe parameters

ty: Expr

Type of the axiom

Definition

Definition: has a computational value

Fields

name: Name

Name of the definition

univ_params: Vec<Name>

Universe parameters

ty: Expr

Type of the definition

val: Expr

Value/body of the definition

hint: ReducibilityHint

Reducibility hint

Theorem

Theorem: like definition but value is a proof (typically opaque)

Fields

name: Name

Name of the theorem

univ_params: Vec<Name>

Universe parameters

ty: Expr

Type of the theorem (the proposition)

val: Expr

Proof of the theorem

Opaque

Opaque: definition that should never be unfolded

Fields

name: Name

Name of the opaque definition

univ_params: Vec<Name>

Universe parameters

ty: Expr

Type of the definition

val: Expr

Value of the definition (hidden)

Implementations

impl Declaration

pub fn name(&self) -> &Name

Get the name of this declaration.

pub fn ty(&self) -> &Expr

Get the type of this declaration.

pub fn univ_params(&self) -> &[Name]

Get the universe parameters.

pub fn value(&self) -> Option<&Expr>

Get the value (if this is a definition/theorem/opaque).

pub fn reducibility_hint(&self) -> ReducibilityHint

Get the reducibility hint.

pub fn to_constant_info(&self) -> ConstantInfo

Convert a legacy Declaration to ConstantInfo.

Trait Implementations

impl Clone for Declaration

fn clone(&self) -> Declaration

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Declaration

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

Formats the value using the given formatter.