You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
As discussed in #17,
Pruviloj
, as currently used in theTactics
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
rewrite
s), rename the chapter to smth likePatternMatching
and keep the original half as an appendix namedTactics
or evenPruviloj
.The text was updated successfully, but these errors were encountered: