1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
|
Set Implicit Arguments.
Set Universe Polymorphism.
Module success.
Unset Primitive Projections.
Record group :=
{ carrier : Type;
id : carrier }.
Notation "1" := (id _) : g_scope.
Delimit Scope g_scope with g.
Bind Scope g_scope with carrier.
Section foo.
Variable g : group.
Variable comp : carrier g -> carrier g -> carrier g.
Check comp 1 1.
End foo.
End success.
Module failure.
Set Primitive Projections.
Record group :=
{ carrier : Type;
id : carrier }.
Notation "1" := (id _) : g_scope.
Delimit Scope g_scope with g.
Bind Scope g_scope with carrier.
Section foo.
Variable g : group.
Variable comp : carrier g -> carrier g -> carrier g.
Check comp 1 1.
(* Toplevel input, characters 11-12:
Error:
In environment
g : group
comp : carrier g -> carrier g -> carrier g
The term "1" has type "nat" while it is expected to have type "carrier g".
*)
End foo.
End failure.
|
