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).
|
