pyk.ktool.claim_loader module

class ClaimLoader(kprove: KProve)[source]

Bases: object

Load and cache spec files as JSON.

load_claims(spec_file: Path, *, spec_module_name: str | None = None, include_dirs: Iterable[Path] = (), md_selector: str | None = None, claim_labels: Iterable[str] | None = None, exclude_claim_labels: Iterable[str] | None = None, include_dependencies: bool = True, type_inference_mode: TypeInferenceMode | None = None) → list[KClaim][source]

Attempt to load a spec from JSON, write file on cache miss.

Parameters:

  • spec_file – Spec file to load.

  • spec_module_name (optional) – Spec module to load.

  • include_dirs (optional) – Includes.

  • md_selector (optional) – Selector expression for Markdown tags.

  • claim_labels (optional) – Claim labels to include in the result.

  • exclude_claim_labels (optional) – Claim labels to exclude from the result.

  • include_dependencies (optional) – If True, claim dependencies are transitively included.

  • type_inference_mode (optional) – Type inference mode.