pyk.ktool.kprove module
- class KProve(definition_dir: Path, main_file: Path | None = None, use_directory: Path | None = None, command: str = 'kprove', bug_report: BugReport | None = None, extra_unparsing_modules: Iterable[KFlatModule] = (), patch_symbol_table: Callable[[SymbolTable], None] | None = None)[source]
Bases:
KPrint- get_claim_index(spec_file: Path, spec_module_name: str | None = None, include_dirs: Iterable[Path] = (), md_selector: str | None = None, type_inference_mode: TypeInferenceMode | None = None) ClaimIndex[source]
- get_claim_modules(spec_file: Path, spec_module_name: str | None = None, include_dirs: Iterable[Path] = (), md_selector: str | None = None, type_inference_mode: TypeInferenceMode | None = None) KFlatModuleList[source]
- get_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]
- main_file: Path | None
- prove(spec_file: Path, spec_module_name: str | None = None, args: Iterable[str] = (), include_dirs: Iterable[Path] = (), md_selector: str | None = None, haskell_args: Iterable[str] = (), depth: int | None = None) list[CTerm][source]
- prove_claim(claim: KClaim, claim_id: str, lemmas: Iterable[KRule] = (), args: Iterable[str] = (), haskell_args: Iterable[str] = (), depth: int | None = None) list[CTerm][source]
- prover: list[str]
- prover_args: list[str]