Struct LfscProof 

pub struct LfscProof { /* private fields */ }

An LFSC proof

Implementations

impl LfscProof

pub fn new() -> Self

Create a new empty LFSC proof

pub fn declare_sort(&mut self, name: impl Into<String>, arity: u32)

Add a sort declaration

pub fn declare_const(&mut self, name: impl Into<String>, sort: LfscSort)

Add a constant declaration

pub fn define( &mut self, name: impl Into<String>, sort: LfscSort, value: LfscTerm, )

Add a definition

pub fn declare_rule( &mut self, name: impl Into<String>, params: Vec<(String, LfscSort)>, conclusion: LfscTerm, )

Add a proof rule declaration

pub fn side_condition( &mut self, name: impl Into<String>, params: Vec<(String, LfscSort)>, return_sort: LfscSort, body: impl Into<String>, )

Add a side condition program

pub fn check(&mut self, term: LfscTerm)

Add a proof check

pub fn len(&self) -> usize

Get the number of declarations

pub fn is_empty(&self) -> bool

Check if the proof is empty

pub fn decls(&self) -> &[LfscDecl]

Get the declarations

pub fn clear(&mut self)

Clear all declarations

pub fn write<W: Write>(&self, writer: W) -> Result<()>

Write the proof in LFSC format

pub fn to_string(&self) -> String

Convert to string

Trait Implementations

impl Debug for LfscProof

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

Formats the value using the given formatter.

impl Default for LfscProof

fn default() -> LfscProof

Returns the “default value” for a type.