5 name = "proofFormatMode"
7 long = "proof-format-mode=MODE"
8 type = "ProofFormatMode"
10 help = "select language of proof output"
11 help_mode = "Proof format modes."
14 help = "Do not translate proof output"
17 help = "Output DOT proof"
20 help = "Output veriT proof"
23 name = "proofPrintConclusion"
25 long = "proof-print-conclusion"
28 help = "Print conclusion of proof steps when printing AST"
31 name = "proofPedantic"
33 long = "proof-pedantic=N"
36 help = "assertion failure for any incorrect rule application or untrusted lemma having pedantic level <=N with proof"
39 name = "proofEagerChecking"
41 long = "proof-eager-checking"
44 help = "check proofs eagerly with proof for local debugging"
47 name = "proofGranularityMode"
49 long = "proof-granularity=MODE"
50 type = "ProofGranularityMode"
51 default = "THEORY_REWRITE"
52 help = "modes for proof granularity"
53 help_mode = "Modes for proof granularity."
56 help = "Do not improve the granularity of proofs."
57 [[option.mode.REWRITE]]
59 help = "Allow rewrite or substitution steps, expand macros."
60 [[option.mode.THEORY_REWRITE]]
61 name = "theory-rewrite"
62 help = "Allow theory rewrite steps, expand macros, rewrite and substitution steps."
63 [[option.mode.DSL_REWRITE]]
65 help = "Allow DSL rewrites and evaluation steps, expand macros, rewrite, substitution, and theory rewrite steps."