blob: 2ad8b924eb9dedcaa41d7a8a784fa438d483bf42 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
(* 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).
End testSection.
(* Check the removal of coercions with target Funclass *)
Record foo : Type := { D :> nat -> nat }.
Check [x:foo;n:nat](x n).
|
