blob: bd7474285707b8aeec978f4227b131e328eb635b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
(* 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.
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.
|
