Crate xpile_contract_backend 

ContractBackend trait — proof-lane rendering abstraction.

Renders parsed xpile_contracts::Contract into LaTeX (math + theorem environments), Lean 4 theorem text (with @[xpile_contract] attribute carrying the verbatim contract ID), or mdBook.

Architectural invariants codified in contracts/xpile-contract-backend-trait-v1.yaml. The citation bridge uses format-native structured constructs parseable by the host elaborator/parser, NOT regex over body text. See docs/specifications/sub/contract-backend-trait.md §“Citation bridge”.

Structs

ContractRenderConfig

Configuration passed to ContractBackend::render.

RenderedDoc

Rendered output of a single contract.

Enums

ContractBackendError

Traits

ContractBackend

Proof-lane rendering trait. See docs/specifications/sub/contract-backend-trait.md.