blob: 2dea0d18528df28555a0bccb187d2672cbfbc0af (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
Set Implicit Arguments.
(* Suggested by Pierre Casteran (bug #169) *)
(* Argument 3 is needed to typecheck and should be printed *)
Definition compose := [A,B,C:Set; f : A-> B ; g : B->C ; x : A] (g (f x)).
Check (compose 3!nat S).
(* Better to explicitly display the arguments inferable from a
position that could disappear after reduction *)
Inductive ex [A:Set;P:A->Prop] : Prop
:= ex_intro : (x:A)(P x)->(ex P).
Check (ex_intro 2![_]True 3!O I).
(* Test for V8 printing of implicit by names *)
Definition d1 [y;x;h:x=y:>nat] := h.
Definition d2 [x] := (!d1 x).
Print d2.
|
