blob: 00230bfc4649b6e15e7c743c7d19547edb643342 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
(* Implicit on section variables *)
Set Implicit Arguments.
(* Example submitted by David Nowak *)
Section Spec.
Variable A:Set.
Variable op : (A:Set)A->A->Set.
Infix 6 "#" op V8only (at level 70).
Check (x:A)(x # x).
(* Example submitted by Christine *)
Record stack : Type := {type : Set; elt : type;
empty : type -> bool; proof : (empty elt)=true }.
Check (type:Set; elt:type; empty:(type->bool))(empty elt)=true->stack.
End Spec.
|
