aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/ImplicitTactic.v
blob: d8fa3043de1995deb69800cc76a819735bd9f9f3 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
(* 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).