Enum ProofRule 

pub enum ProofRule {
    Conjunction,
    DisjunctionCheck {
        detail: String,
    },
    DisjunctionIntro {
        side: String,
    },
    Negation,
    ModalPassthrough {
        kind: String,
    },
    ExistsWitness {
        var: String,
        term: LogicalTerm,
    },
    ExistsFailed,
    ForallVacuous,
    ForallVerified {
        entities: Vec<LogicalTerm>,
    },
    ForallCounterexample {
        entity: LogicalTerm,
    },
    CountResult {
        expected: u32,
        actual: u32,
    },
    PredicateCheck {
        method: String,
        detail: String,
    },
    ComputeCheck {
        method: String,
        detail: String,
    },
    Asserted {
        fact: String,
    },
    Derived {
        label: String,
        fact: String,
    },
    ProofRef {
        fact: String,
    },
    EqualitySubstitution {
        original: String,
        equality_facts: String,
        substituted: String,
    },
    RuleAttemptFailed {
        rule_label: String,
        failed_condition: String,
    },
    PredicateNotFound {
        predicate: String,
    },
}

Proof rule applied at a single proof step.

This IS the serde wire type (named fields, #[serde(tag = "type")]): the same type crosses every native boundary (nibli-reason → nibli-engine/nibli-wasm → JSON → nibli-ui). nibli-protocol re-exports it and owns only the JSON helpers; the WIT boundary (nibli-pipeline/nibli-host) keeps its generated tuple-shaped mirror by necessity. The serde attributes are the JSON contract — do not rename a field or tag.

Variants

Conjunction

DisjunctionCheck

Fields

detail: String

DisjunctionIntro

Fields

side: String

Negation

ModalPassthrough

Fields

kind: String

ExistsWitness

Fields

var: String

term: LogicalTerm

ExistsFailed

ForallVacuous

ForallVerified

Fields

entities: Vec<LogicalTerm>

ForallCounterexample

Fields

entity: LogicalTerm

CountResult

Fields

expected: u32

actual: u32

PredicateCheck

Fields

method: String

detail: String

ComputeCheck

Fields

method: String

detail: String

Asserted

Fields

fact: String

Derived

Fields

label: String

fact: String

ProofRef

Fields

fact: String

EqualitySubstitution

Equality substitution: fact proved by substituting equivalent terms. Fields: original fact, equality facts used, substituted fact that was found.

Fields

original: String

equality_facts: String

substituted: String

RuleAttemptFailed

Rule was tried but a condition failed.

Fields

rule_label: String

failed_condition: String

PredicateNotFound

Predicate not found in fact store and no rule could derive it.

Fields

predicate: String

Trait Implementations

impl Clone for ProofRule

fn clone(&self) -> ProofRule

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofRule

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

Formats the value using the given formatter.

impl PartialEq for ProofRule

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for ProofRule