test-suite/success/implicit.v


1
2
3
4
5
6
7
8
9

(* Implicit on section variables *)
(* Example submitted by David Nowak *)

Set Implicit Arguments.
Section Spec.
Variable A:Set.
Variable op : (A:Set)A->A->Set.
Infix 6 "#" op.
Check (x:A)(x # x).