37 lines
688 B
Rust
37 lines
688 B
Rust
/*#[derive(Clone, Copy, Eq, Hash, PartialEq)]
|
|
pub enum ProofDirection
|
|
{
|
|
Forward,
|
|
Backward,
|
|
}
|
|
|
|
#[derive(Eq, Hash, PartialEq)]
|
|
pub enum CompletionTarget
|
|
{
|
|
Predicate(std::rc::Rc<foliage::PredicateDeclaration>),
|
|
Constraint,
|
|
}
|
|
|
|
pub struct CompletionFormula
|
|
{
|
|
pub target: CompletionTarget,
|
|
pub formula: foliage::Formula,
|
|
}
|
|
|
|
pub struct Lemma
|
|
{
|
|
pub direction: Option<ProofDirection>,
|
|
pub formula: foliage::Formula,
|
|
}
|
|
|
|
pub struct Specification
|
|
{
|
|
pub axioms: foliage::Formulas,
|
|
pub lemmas: Vec<Lemma>,
|
|
pub assumptions: foliage::Formulas,
|
|
pub assertions: foliage::Formulas,
|
|
|
|
pub input_constants: foliage::FunctionDeclarations,
|
|
pub input_predicates: foliage::PredicateDeclarations,
|
|
}*/
|