blob: d7ea72271e140af9a83273bded8fae3957b7ad46 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
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).
|
