Enum SerialDecl 

pub enum SerialDecl {
    Axiom {
        name: String,
        kind_tag: u8,
    },
    Definition {
        name: String,
        kind_tag: u8,
    },
    Theorem {
        name: String,
        kind_tag: u8,
    },
    Opaque {
        name: String,
        kind_tag: u8,
    },
    Inductive {
        name: String,
        ctor_count: u32,
        kind_tag: u8,
    },
    Other {
        name: String,
        kind_tag: u8,
    },
}

A serializable record for a kernel declaration.

Variants

Axiom

Fields

name: String

kind_tag: u8

Definition

Fields

name: String

kind_tag: u8

Theorem

Fields

name: String

kind_tag: u8

Opaque

Fields

name: String

kind_tag: u8

Inductive

Fields

name: String

ctor_count: u32

kind_tag: u8

Other

Fields

name: String

kind_tag: u8

Implementations

impl SerialDecl

pub fn name(&self) -> &str

Return the declaration’s name.

pub fn kind_tag(&self) -> u8

Return the declaration’s kind tag byte.

Trait Implementations

impl Clone for SerialDecl

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SerialDecl

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

Formats the value using the given formatter.

impl PartialEq for SerialDecl

fn eq(&self, other: &Self) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for SerialDecl