Split/rewrite Tactics?
clayrat opened this issue · 1 comments
clayrat commented
As discussed in #17, Pruviloj, as currently used in the Tactics chapter is probably too experimental to be introduced so early in the book.
My proposal is to re-do the first half with dependent pattern matching (possibly discussing its use vs rewrites), rename the chapter to smth like PatternMatching and keep the original half as an appendix named Tactics or even Pruviloj.
yurrriq commented
I've got a couple minor edits of Tactics to PR.