Module error 

Error types for proof search and unification.

This module defines ProofError, which captures all failure modes during proof construction. Errors are designed to be informative for debugging and educational feedback.

Error Categories

Category	Variants	Meaning
Search	NoProofFound, DepthExceeded	Proof search terminated
Unification	OccursCheck, UnificationFailed, ExprUnificationFailed	Terms cannot be unified
Matching	SymbolMismatch, ArityMismatch	Structural incompatibility
Higher-Order	PatternNotDistinct, NotAPattern, ScopeViolation	Miller pattern failures

Example

use logicaffeine_proof::ProofError;

fn check_result(result: Result<(), ProofError>) {
    match result {
        Ok(()) => println!("Proof found"),
        Err(ProofError::NoProofFound) => println!("No proof exists"),
        Err(ProofError::DepthExceeded) => println!("Search too deep"),
        Err(e) => println!("Error: {}", e),
    }
}

Enums

ProofError

Errors that can occur during proof search.

Type Aliases

ProofResult

Result type for proof operations.