From: Andrea Berlingieri Date: Thu, 25 Apr 2019 13:07:24 +0000 (+0200) Subject: Add last declarative tactics, modify rewriting tactics X-Git-Tag: make_still_working~229^2~1^2~1^2~6 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=489639a3c319d0349a9c864fd0eeaf659daa3d3f;hp=489639a3c319d0349a9c864fd0eeaf659daa3d3f;p=helm.git Add last declarative tactics, modify rewriting tactics Add types for induction and case analysis to grafiteAst. Add new types for obtain and conclude Add pp code for induction, case, obtain, conclude Add calls in grafiteEngine for induction, case, obtain, conclude Add parsing rules for induction, case, obtain, conclude Rename a function for code clarity Add function to swap two goals on the stack (useful for obtain) Add a conclude function that checks that the given term is the lhs of the current goal Add a obtain function that starts an equality chain beginning with the given term in a new goal Modify rewriting step to only handle single equality chains steps Add implementation for induction and case. Add signatures for induction, case, conclude, obtain Add keywords to matita.lang for induction, case, conclude, obtain ---