Tactics and Automation
There are two parts to this chapter. The first part presents several collections of tactics specialized in various domains of logic and mathematics: tactics specialized in reasoning about inductive types, the main automatic tactics, which rely on a Prolog-like proof search mechanism, the tactics for equality and rewriting, the tactics for numerical proofs, and the automatic decision procedures for restricted fragments of logic.
KeywordsPattern Match Finished Transaction Choice Point Inductive Type Proof Search
Unable to display preview. Download preview PDF.