search

lukaszcz / coqhammer

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
Other
217 stars 31 forks source link

Documentation for best #129

Closed brando90 closed 2 years ago

brando90 commented 2 years ago

Apologies for the bombardment of issues.

Can we have best to have its own documentation here https://coqhammer.github.io/#tutorial like sauto, hammer?

Thanks! Cool tool! :)

lukaszcz commented 2 years ago

You mean making a video tutorial for "best"? It would make sense to incorporate it into the "sauto" video tutorial, but I'm not going to re-record the tutorial ("best" was added after I made the tutorial). "best" is mentioned in the "Tutorial" section and described in the "Sauto" section of the documentation, and there is little to it in terms of usage. You just run it and copy the result if it works. It accepts the same options as "sauto" plus the "time:" option.