]>
matita.cs.unibo.it Git - helm.git/commit
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