tokitai-operator 0.1.0

//! IR-level contract and theory-requirement types.
//!
//! `IRContract` is the per-node contract expression that the IR
//! builds from the op-level contracts. `CertifiedTheoryRequirement`
//! is the abstract requirement that an IR node must satisfy
//! (e.g. "the input valuation cutoff is the active precision").
//!
//! These types bridge `src/domain/contract.rs` (the abstract
//! contract primitives) and `src/ir/semantic.rs` (the actual
//! `SemanticGraph`).
//!
use crate::domain::{Condition, ContractId};
use crate::theory::CertifiedTheoryRequirement;

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct RewriteJustification {
    pub source: ContractId,
    pub rule: String,
    pub discharged_conditions: Vec<Condition>,
    pub certified_requirements: Vec<CertifiedTheoryRequirement>,
}