1
Set Implicit Arguments.
4
(* Suggested by Pierre Casteran (bug #169) *)
5
(* Argument 3 is needed to typecheck and should be printed *)
6
Definition compose (A B C : Set) (f : A -> B) (g : B -> C) (x : A) := g (f x).
7
Check (compose (C:=nat) S).
9
(* Better to explicitly display the arguments inferable from a
10
position that could disappear after reduction *)
11
Inductive ex (A : Set) (P : A -> Prop) : Prop :=
12
ex_intro : forall x : A, P x -> ex P.
13
Check (ex_intro (P:=fun _ => True) (x:=0) I).
15
(* Test for V8 printing of implicit by names *)
16
Definition d1 y x (h : x = y :>nat) := h.
17
Definition d2 x := d1 (y:=x).
21
(* Check maximal insertion of implicit *)
25
Open Scope list_scope.
27
Set Implicit Arguments.
28
Set Maximal Implicit Insertion.
30
Definition id (A:Type) (x:A) := x.
32
Check map id (1::nil).
34
Definition id' (A:Type) (x:A) := x.
36
Implicit Arguments id' [[A]].
38
Check map id' (1::nil).