3
Structure foo : Type := Foo {
4
A : Set; Aopt := option A; unopt : Aopt -> A
7
Canonical Structure unopt_nat := @Foo nat (fun _ => O).
9
(* Granted wish #1187 *)
11
Record Silly (X : Set) : Set := mkSilly { x : X }.
12
Definition anotherMk := mkSilly.
13
Definition struct := anotherMk nat 3.
14
Canonical Structure struct.
16
(* Intertwinning canonical structures and delta-expansion *)
17
(* Assia's short example *)
19
Open Scope bool_scope.
21
Set Implicit Arguments.
23
Structure test_struct : Type := mk_test {dom :> Type; f : dom -> dom -> bool}.
25
Notation " x != y":= (f _ x y)(at level 10).
27
Canonical Structure bool_test := mk_test (fun x y => x || y).
31
Check (fun x : b => x != x).