search

RedPRL / sml-dependent-lcf

A library for the next generation of LCF refiners, with support for dependent refinement—Long Live the Anti-Realist Struggle!
16 stars 1 forks source link

Warning for too many tactics in `[_, _, ..., _]` #44

Closed favonia closed 1 year ago

favonia commented 6 years ago

https://github.com/RedPRL/sml-redprl/issues/592

favonia commented 6 years ago

Is there a way to warn users now instead of the tactic being failing?