Module validation 

Semantic validation for Lemma specs

Validates spec structure and type declarations to catch errors early with clear messages.

Structs

RuleEntryForBindingCheck

Rule data needed to validate spec interfaces (avoids validation depending on graph).

Functions

validate_spec_interfaces

Validate that every spec-ref fact path’s referenced spec has the required rules and that each such rule’s result type satisfies what the referencing rules expect. Type errors are reported at the binding fact’s source when a binding changed the spec ref.

validate_type_specifications

Validate that TypeSpecification constraints are internally consistent