document RuleApplication

src/common.rs

@@ -28,12 +28,21 @@ where
 }
 
 #[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
+/// A proof element that has yet to be translated to a presentable form.
+///
+/// [crate::prove::prove] function does not immediately convert LowRuleApplication's to
+/// [RuleApplication]'s. Rather, it converts only the LowRuleApplication's it is going to return
+/// to the caller.
 pub struct LowRuleApplication {
     pub rule_index: usize,
     pub instantiations: BTreeMap<usize, usize>,
 }
 
 impl LowRuleApplication {
+    /// Translate to a higher representation [RuleApplication]. The higher representation is
+    /// portable to other machines as long as those machines assume the same rule list.
+    /// This lower representation is not portable.
+    ///
     /// Panics
     ///
     /// This function will panic if:

src/prove.rs

@@ -211,6 +211,37 @@ impl std::error::Error for CantProve {}
 
 #[derive(Debug, PartialEq, Eq)]
 #[cfg_attr(feature = "serde", derive(serde::Deserialize, serde::Serialize))]
+/// 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 `instanitations`. They are bound in order of
+/// initial appearance.
+///
+/// Given the rule:
+///
+/// ```customlang
+/// ifall
+///   [?z ex:foo ?x DG]
+/// then
+///   [?x ex:bar ?z DG]
+/// ```
+///
+/// and the RuleApplication:
+///
+/// ```customlang
+/// RuleApplication {
+///   rule_index: 0,
+///   instantiations: vec!["foer", "bary"],
+/// }
+/// ```
+///
+/// The rule application represents the deductive proof:
+///
+/// ```customlang
+/// [foer ex:foo bary DG]
+/// therefore
+/// [bary ex:bar foer DG]
+/// ```
 pub struct RuleApplication<Bound> {
     /// The index of the rule in the implicitly associated rule list.
     pub rule_index: usize,