diff options
author | 2005-09-09 22:07:24 +0000 | |
---|---|---|
committer | 2005-09-09 22:07:24 +0000 | |
commit | b7f6c7c76571bff4f452d2c48d64be4e15878e11 (patch) | |
tree | 8b2a5f76bf1c5a7f3c5383a8cd8d28e91e9330a9 /test-suite/success | |
parent | 2d3335cbd6a34f8d5d3c7444a68dba7399d817a7 (diff) |
Declare Implicit Tactic
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7366 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success')
-rw-r--r-- | test-suite/success/ImplicitTactic.v8 | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/success/ImplicitTactic.v8 b/test-suite/success/ImplicitTactic.v8 new file mode 100644 index 000000000..ccdc0be34 --- /dev/null +++ b/test-suite/success/ImplicitTactic.v8 @@ -0,0 +1,15 @@ +(* A Wiedijk-Cruz-Filipe style tactic for solving implicit arguments *) + +(* Declare a term expression with a hole *) +Parameter quo : nat -> forall n:nat, n<>0 -> nat. +Notation "x / y" := (quo x y _) : nat_scope. + +(* Declare the tactic for resolving implicit arguments still + unresolved after type-checking; it must complete the subgoal to + succeed *) +Declare Implicit Tactic assumption. + +Goal forall n d, d<>0 -> { q:nat & { r:nat | d * q + r = n }}. +intros. +(* Here, assumption is used to solve the implicit argument of quo *) +exists (n / d). |