Struct mm0b_parser::ThmEntry

#[repr(C, align(8))]
pub struct ThmEntry {
    pub num_args: U16<LE>,
    pub reserved: [u8; 2],
    pub p_args: U32<LE>,
}

An entry in the theorem table, which describes the “signature” of the axiom/theorem, the information needed to apply the theorem to use it in other theorems.

Fields

num_args: U16<LE>

The number of arguments to the theorem (exprs, not hyps).

reserved: [u8; 2]

Padding.

p_args: U32<LE>

The pointer to an args: [Arg; num_args] array, followed by the theorem’s unify command sequence.

Trait Implementations

impl AsBytes for ThmEntry

fn only_derive_is_allowed_to_implement_this_trait() where
    Self: Sized, 

fn as_bytes(&self) -> &[u8]

Get the bytes of this value.

fn as_bytes_mut(&mut self) -> &mut [u8] where
    Self: FromBytes, 

Get the bytes of this value mutably.

impl Clone for ThmEntry

fn clone(&self) -> ThmEntry

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for ThmEntry

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

Formats the value using the given formatter.

impl FromBytes for ThmEntry

fn only_derive_is_allowed_to_implement_this_trait() where
    Self: Sized, 

impl Copy for ThmEntry