Disable proof search when inlining

advancedresearch / poi

a pragmatic point-free theorem prover assistant

Apache License 2.0

136 stars 7 forks source link

Open bvssvni opened 3 years ago

bvssvni commented 3 years ago

Currently, inlining takes long time to complete, because proof search is enabled.

When running scripts, one does not want inlining to be slow, because usually enough subgoals are specified to make proof search fast.