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 help = "Output TPTP proof (work in progress)"
26 name = "proofPrintConclusion"
28 long = "proof-print-conclusion"
31 help = "Print conclusion of proof steps when printing AST"
34 name = "proofPedantic"
36 long = "proof-pedantic=N"
39 help = "assertion failure for any incorrect rule application or untrusted lemma having pedantic level <=N with proof"
44 long = "proof-check=MODE"
45 type = "ProofCheckMode"
47 help = "select proof checking mode"
48 help_mode = "Proof checking modes."
51 help = "check rule applications and proofs from generators eagerly for local debugging"
52 [[option.mode.EAGER_SIMPLE]]
54 help = "check rule applications during construction"
57 help = "check rule applications only during final proof construction"
60 help = "do not check rule applications"
63 name = "proofGranularityMode"
65 long = "proof-granularity=MODE"
66 type = "ProofGranularityMode"
67 default = "THEORY_REWRITE"
68 help = "modes for proof granularity"
69 help_mode = "Modes for proof granularity."
72 help = "Do not improve the granularity of proofs."
73 [[option.mode.REWRITE]]
75 help = "Allow rewrite or substitution steps, expand macros."
76 [[option.mode.THEORY_REWRITE]]
77 name = "theory-rewrite"
78 help = "Allow theory rewrite steps, expand macros, rewrite and substitution steps."
79 [[option.mode.DSL_REWRITE]]
81 help = "Allow DSL rewrites and evaluation steps, expand macros, rewrite, substitution, and theory rewrite steps."