blob: a833dd0bd6095a0ecb475f738f24072d8d96f7ea (
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
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
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
|
(* Bug #1172 *)
Structure foo : Type := Foo {
A : Set; Aopt := option A; unopt : Aopt -> A
}.
Canonical Structure unopt_nat := @Foo nat (fun _ => O).
(* Granted wish #1187 *)
Record Silly (X : Set) : Set := mkSilly { x : X }.
Definition anotherMk := mkSilly.
Definition struct := anotherMk nat 3.
Canonical Structure struct.
(* Intertwinning canonical structures and delta-expansion *)
(* Assia's short example *)
Open Scope bool_scope.
Set Implicit Arguments.
Structure test_struct : Type := mk_test {dom :> Type; f : dom -> dom -> bool}.
Notation " x != y":= (f _ x y)(at level 10).
Canonical Structure bool_test := mk_test (fun x y => x || y).
Definition b := bool.
Check (fun x : b => x != x).
Inductive four := x0 | x1 | x2 | x3.
Structure local := MKL { l : four }.
Section X.
Definition s0 := MKL x0.
#[local] Canonical Structure s0.
Check (refl_equal _ : l _ = x0).
#[local] Canonical Structure s1 := MKL x1.
Check (refl_equal _ : l _ = x1).
Local Canonical Structure s2 := MKL x2.
Check (refl_equal _ : l _ = x2).
End X.
Fail Check (refl_equal _ : l _ = x0).
Fail Check (refl_equal _ : l _ = x1).
Fail Check (refl_equal _ : l _ = x2).
Check s0.
Check s1.
Check s2.
Section Y.
Let s3 := MKL x3.
Canonical Structure s3.
Check (refl_equal _ : l _ = x3).
End Y.
Fail Check (refl_equal _ : l _ = x3).
Fail Check s3.
Section V.
#[canonical] Let s3 := MKL x3.
Check (refl_equal _ : l _ = x3).
End V.
Section W.
#[canonical, local] Definition s2' := MKL x2.
Check (refl_equal _ : l _ = x2).
End W.
Fail Check (refl_equal _ : l _ = x2).
(* Lambda keys *)
Section L1.
Structure cs_lambda := { cs_lambda_key : nat -> nat }.
#[local] Canonical Structure cs_lambda_func :=
{| cs_lambda_key := fun x => x + 1 |}.
Check (refl_equal _ : cs_lambda_key _ = fun _ => _ + _).
End L1.
Section L2.
#[local] Canonical Structure cs_lambda_func2 :=
{| cs_lambda_key := fun x => 1 + x |}.
Check (refl_equal _ : cs_lambda_key _ = fun x => 1 + x).
End L2.
Section L3.
#[local] Canonical Structure cs_lambda_func3 :=
{| cs_lambda_key := fun x => 1 + x |}.
Check (refl_equal _ : cs_lambda_key _ = Nat.add 1).
End L3.
Section L4.
#[local] Canonical Structure cs_lambda_func4 :=
{| cs_lambda_key := Nat.add 1 |}.
Check (refl_equal _ : cs_lambda_key _ = Nat.add 1).
End L4.
Section L5.
#[local] Canonical Structure cs_lambda_func5 :=
{| cs_lambda_key := Nat.add 1 |}.
Check (refl_equal _ : cs_lambda_key _ = fun x => 1 + x).
End L5.
|
