Enum LfscDecl 

pub enum LfscDecl {
    DeclareSort {
        name: String,
        arity: u32,
    },
    DeclareConst {
        name: String,
        sort: LfscSort,
    },
    Define {
        name: String,
        sort: LfscSort,
        value: LfscTerm,
    },
    DeclareRule {
        name: String,
        params: Vec<(String, LfscSort)>,
        conclusion: LfscTerm,
    },
    SideCondition {
        name: String,
        params: Vec<(String, LfscSort)>,
        return_sort: LfscSort,
        body: String,
    },
    Check(LfscTerm),
}

An LFSC declaration

Variants

DeclareSort

Declare a new sort

Fields

name: String

arity: u32

DeclareConst

Declare a new constant/function

Fields

name: String

sort: LfscSort

Define

Define a term

Fields

name: String

sort: LfscSort

value: LfscTerm

DeclareRule

Declare a proof rule

Fields

name: String

params: Vec<(String, LfscSort)>

conclusion: LfscTerm

SideCondition

Side condition program

Fields

name: String

params: Vec<(String, LfscSort)>

return_sort: LfscSort

body: String

Check(LfscTerm)

Proof step (check)

Trait Implementations

impl Clone for LfscDecl

fn clone(&self) -> LfscDecl

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LfscDecl

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

Formats the value using the given formatter.

impl Display for LfscDecl

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

Formats the value using the given formatter.