summaryrefslogtreecommitdiff
path: root/src/options/proof_options.toml
diff options
context:
space:
mode:
Diffstat (limited to 'src/options/proof_options.toml')
-rw-r--r--src/options/proof_options.toml16
1 files changed, 16 insertions, 0 deletions
diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml
index 3eb32060e..8eb2fd783 100644
--- a/src/options/proof_options.toml
+++ b/src/options/proof_options.toml
@@ -92,6 +92,22 @@ name = "Proof"
help = "Allow DSL rewrites and evaluation steps, expand macros, rewrite, substitution, and theory rewrite steps."
[[option]]
+ name = "proofAnnotate"
+ category = "regular"
+ long = "proof-annotate"
+ type = "bool"
+ default = "false"
+ help = "add optional annotations to proofs, which enables statistics for inference ids for lemmas and conflicts appearing in final proof"
+
+[[option]]
+ name = "proofPruneInput"
+ category = "regular"
+ long = "proof-prune-input"
+ type = "bool"
+ default = "false"
+ help = "Prune unused input assumptions from final scope"
+
+[[option]]
name = "proofAletheResPivots"
category = "regular"
long = "proof-alethe-res-pivots"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback