blob: b6c9f053f3d145f6a9201dc296b71aaf4364e05d (
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
|
From mathcomp Require Import all_ssreflect all_algebra all_field.
Section regular.
Import GRing.
Let eq_ringType_of_regular_lalgType (R : ringType) :=
erefl : regular_lalgType R = Ring.Pack (Ring.class R) :> ringType.
Let eq_ringType_of_regular_algType (R : comRingType) :=
erefl : regular_algType R = Ring.Pack (Ring.class R) :> ringType.
Let eq_comRingType_of_regular_comAlgType (R : comRingType) :=
erefl : regular_comAlgType R = ComRing.Pack (ComRing.class R) :> ringType.
Let eq_unitRingType_of_regular_unitAlgType (R : comUnitRingType) :=
erefl : regular_unitAlgType R =
UnitRing.Pack (UnitRing.class R) :> unitRingType.
(* The following assertion fails if the class records are not primitive *)
(* because the [comUnitAlgType _ of _] packager inserts an eta-expansion on *)
(* the class. *)
Let eq_comUnitRingType_of_regular_comUnitAlgType (R : comUnitRingType) :=
erefl : regular_comUnitAlgType R =
ComUnitRing.Pack (ComUnitRing.class R) :> comUnitRingType.
Let eq_unitRingType_of_regular_FalgType (R : comUnitRingType) :=
erefl : regular_FalgType R = UnitRing.Pack (UnitRing.class R) :> unitRingType.
(* The following assertion also fails if the class records are not primitive. *)
Let eq_fieldType_of_regular_fieldExtType (K : fieldType) :=
erefl : regular_fieldExtType K = Field.Pack (Field.class K) :> fieldType.
End regular.
|
