blob: 05305d1b2a3f665d01865fd77bb870f12228fbeb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(****************************************************************************)
(* EqDecide.v *)
(* A tactic for deciding propositional equality on inductive types *)
(* by Eduardo Gimenez *)
(****************************************************************************)
(*i $Id$ i*)
Declare ML Module "equality" "eqdecide".
Grammar tactic simple_tactic : ast :=
EqDecideRuleG1
[ "Decide" "Equality" constrarg($com1) constrarg($com2) ] ->
[ (DecideEquality $com1 $com2) ]
| EqDecideRuleG2
[ "Decide" "Equality" ] -> [ (DecideEquality) ]
| CompareRule
[ "Compare" constrarg($com1) constrarg($com2) ] -> [ (Compare $com1 $com2) ].
Syntax tactic level 0:
EqDecideRulePP1
[ <<(DecideEquality)>> ] -> [ "Decide Equality" ]
| EqDecideRulePP2
[ <<(DecideEquality $com1 $com2)>> ] ->
[ "Decide Equality" [1 2] $com1 [1 2] $com2 ]
| ComparePP
[ <<(Compare $com1 $com2)>> ] -> [ "Compare" [1 2] $com1 [1 2] $com2 ].
|
