blob: 0e84bf39663329d2f1bd55a972498eaab4985d77 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
(* 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 (fun (x : foo) (n : nat) => x n).
(* Check both removal of coercions with target Funclass and mixing
string and numeral scopes *)
Require Import String.
Open Scope string_scope.
Inductive PAIR := P (s:string) (n:nat).
Coercion P : string >-> Funclass.
Check ("1" 0).
|
