search

lukaszcz / coqhammer

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

Unfolding of notations #141

Open skogsbaer opened 2 years ago

skogsbaer commented 2 years ago

With unfold, you can unfold notations, e.g. unfold "#".

You can't to this with sauto: sauto unfold:"#" or sauto unfold:# gives a syntax error.