Struct RuleApplication 

pub struct RuleApplication<Bound> {
    pub rule_index: usize,
    pub instantiations: Vec<Bound>,
}

An element of a deductive proof. Proofs can be transmitted and later validatated as long as the validator assumes the same rule list as the prover.

Unbound variables are bound to the values in instantiations. They are bound in order of initial appearance.

Given the rule:

ifall
  [?z ex:foo ?x DG]
then
  [?x ex:bar ?z DG]

and the RuleApplication:

RuleApplication {
  rule_index: 0,
  instantiations: vec!["foer", "bary"],
}

The rule application represents the deductive proof:

[foer ex:foo bary DG]
therefore
[bary ex:bar foer DG]

Fields

rule_index: usize

The index of the rule in the implicitly associated rule list.

instantiations: Vec<Bound>

Bindings for unbound names in the rule in order of appearance.

Trait Implementations

impl<Bound: Debug> Debug for RuleApplication<Bound>

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

Formats the value using the given formatter.

impl<Bound: PartialEq> PartialEq for RuleApplication<Bound>

fn eq(&self, other: &RuleApplication<Bound>) -> bool

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<Bound: Eq> Eq for RuleApplication<Bound>

impl<Bound> StructuralPartialEq for RuleApplication<Bound>