Certified Programming with Dependent Types: book/src/Tactics.v annotate

Nats StackMachine done

author	Adam Chlipala <adamc@hcoop.net>
date	Mon, 01 Sep 2008 12:52:30 -0400
parents	9fea5674367c
children

rev	line source
adamc@2	1 (* Copyright (c) 2008, Adam Chlipala
adamc@2	2 *
adamc@2	3 * This work is licensed under a
adamc@2	4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@2	5 * Unported License.
adamc@2	6 * The license text is available at:
adamc@2	7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@2	8 *)
adamc@2	9
adamc@2	10 Require Import List.
adamc@2	11
adamc@2	12
adamc@2	13 Ltac rewriteHyp :=
adamc@2	14 match goal with
adamc@2	15 \| [ H : _ \|- _ ] => rewrite H
adamc@2	16 end.
adamc@2	17
adamc@2	18 Ltac rewriterP := repeat (rewriteHyp; autorewrite with cpdt in *).
adamc@2	19
adamc@2	20 Ltac rewriter := autorewrite with cpdt in *; rewriterP.
adamc@2	21
adamc@2	22 Hint Rewrite app_ass : cpdt.
adamc@2	23
adamc@2	24 Ltac sintuition := simpl; intuition.
adamc@2	25
adamc@2	26 Ltac crush := sintuition; rewriter; sintuition.

Mercurial > cpdt > repo