yichus lean
Prove supported Bool laws on a configured host with the pinned Lean toolchain
This help is generated from the same argument parser as the CLI. For a
subcommand, append its name and --help to see its options.
Usage: yichus lean [--source <path>]... [--request <path>] --toolchain <path> [--timeout-ms <integer>] [--result <path>] [--json] [--view <string>] [--emit-lean <path>]
Prove supported Bosatsu laws with the pinned Lean toolchain on this host
Options and flags:
--help
Display this help text.
--source <path>
Bosatsu source file (repeatable)
--request <path>
JSON request with sources [{fileName, source}]
--toolchain <path>
Private read-only directory containing the pinned Lean toolchain
--timeout-ms <integer>
Whole proof-worker deadline
--result <path>
Write the proof run artifact here
--json
Print the proof run artifact as JSON
--view <string>
full (default) or compact agent view; compact requires --json and --result
--emit-lean <path>
Save the generated Lean module before checking (one ordinary law); this file is not proof evidence