blob: 61b69038f3735cfc5e7c7183fdaae0e94c679a2e (
plain)
1
2
3
4
5
6
7
8
9
|
(* Submitted by Randy Pollack *)
Record pred [S:Set]: Type := { sp_pred :> S -> Prop }.
Record rel [S:Set]: Type := { sr_rel :> S -> S -> Prop }.
Section testSection.
Variables S: Set; P: (pred S); R: (rel S); x:S.
Check (P x).
Check (R x x).
|
