Struct LeanExportSignature 

pub struct LeanExportSignature { /* private fields */ }

Trusted manifest signature for one Lean export.

Implementations

impl LeanExportSignature

pub fn function( symbol: impl Into<String>, args: impl Into<Vec<LeanExportArgAbi>>, result: LeanExportReturnAbi, ) -> Self

Construct a manifest signature for a function export.

pub fn global(symbol: impl Into<String>, result: LeanExportReturnAbi) -> Self

Construct a manifest signature for a global export.

pub fn symbol(&self) -> &str

Exported symbol name.

pub const fn kind(&self) -> LeanExportSymbolKind

Function/global classification.

pub fn args(&self) -> &[LeanExportArgAbi]

Argument ABI slots.

pub const fn result(&self) -> LeanExportReturnAbi

Result ABI slot.

pub fn to_json(&self) -> Value

Encode as a manifest JSON object.

Trait Implementations

impl Clone for LeanExportSignature

fn clone(&self) -> LeanExportSignature

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LeanExportSignature

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

Formats the value using the given formatter.

impl PartialEq for LeanExportSignature

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

impl StructuralPartialEq for LeanExportSignature