From 562da0c4beec2525db4867e56867576aaf6c0bd8 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Tue, 2 Apr 2019 16:40:14 +0200 Subject: identifying missing joins --- etc/utils/hierarchy_test.py | 46 +++ mathcomp/Make | 1 + mathcomp/test-suite/hierarchy_test.v | 719 +++++++++++++++++++++++++++++++++++ 3 files changed, 766 insertions(+) create mode 100644 etc/utils/hierarchy_test.py create mode 100644 mathcomp/test-suite/hierarchy_test.v diff --git a/etc/utils/hierarchy_test.py b/etc/utils/hierarchy_test.py new file mode 100644 index 0000000..bc90c55 --- /dev/null +++ b/etc/utils/hierarchy_test.py @@ -0,0 +1,46 @@ +#!/usr/bin/python +# usage: hiearchy_test.py inputfile + +import pygraphviz as pgv +import sys, argparse + +def children(G,n): + res = set() + new = set([n]) + while new != set(): + p = new.pop() + res.add(p) + new.update(set(G.successors(p)).difference(res)) + return res + +def common_children(G): + result = set() + for x in G.nodes(): + for y in G.nodes(): + if children(G,x).intersection(children(G,y)) != set(): + result.add((x,y)) + return result + +def print_common_children_coq_check(G): + print("(** Generated by etc/utils/hierarchy_test.py *)") + print("From mathcomp Require Import all.") + for x in G.nodes(): + if x.rfind("Lmod") >= 0 or x.rfind("Splitting") >= 0 or \ + x.rfind("lgebra") >= 0 or x.rfind("FieldExt") >= 0 or \ + x.rfind("Vector") >= 0: + print ("Local Notation \"" + x + ".type\" := (" + x + ".type _).") + print ("") + for (x, y) in common_children(G): + if x < y: + print ("Check erefl : (_ : " + x + ".type) = (_ : " + y + ".type) :> Type.") + +def main(): + parser = argparse.ArgumentParser(description='Generate a check .v file \ + for mathcomp structure hiearchies') + parser.add_argument('dotfile', metavar='', nargs=1, + help='a dotfile representing the hierarchy') + args = parser.parse_args() + print_common_children_coq_check(pgv.AGraph(args.dotfile[0])) + +if __name__ == "__main__": + main() diff --git a/mathcomp/Make b/mathcomp/Make index 147d5b1..27bf34f 100644 --- a/mathcomp/Make +++ b/mathcomp/Make @@ -87,6 +87,7 @@ ssreflect/ssrnat.v ssreflect/ssrnotations.v ssreflect/ssrmatching.v ssreflect/tuple.v +test-suite/hierarchy_test.v -I . -R . mathcomp diff --git a/mathcomp/test-suite/hierarchy_test.v b/mathcomp/test-suite/hierarchy_test.v new file mode 100644 index 0000000..0085018 --- /dev/null +++ b/mathcomp/test-suite/hierarchy_test.v @@ -0,0 +1,719 @@ +(** Generated by etc/utils/hierarchy_test.py *) +From mathcomp Require Import all. +Local Notation "FinRing.UnitAlgebra.type" := (FinRing.UnitAlgebra.type _). +Local Notation "GRing.Lalgebra.type" := (GRing.Lalgebra.type _). +Local Notation "FinRing.Lalgebra.type" := (FinRing.Lalgebra.type _). +Local Notation "FinRing.Algebra.type" := (FinRing.Algebra.type _). +Local Notation "FieldExt.type" := (FieldExt.type _). +Local Notation "GRing.UnitAlgebra.type" := (GRing.UnitAlgebra.type _). +Local Notation "FinRing.Lmodule.type" := (FinRing.Lmodule.type _). +Local Notation "GRing.Algebra.type" := (GRing.Algebra.type _). +Local Notation "SplittingField.type" := (SplittingField.type _). +Local Notation "Falgebra.type" := (Falgebra.type _). +Local Notation "GRing.Lmodule.type" := (GRing.Lmodule.type _). +Local Notation "Vector.type" := (Vector.type _). + +Check erefl : (_ : CountRing.ComRing.type) = (_ : FinGroup.type) :> Type. +Check erefl : (_ : FieldExt.type) = (_ : SplittingField.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : GRing.Field.type) :> Type. +Check erefl : (_ : Num.NumField.type) = (_ : Num.RealClosedField.type) :> Type. +Check erefl : (_ : FinRing.Lalgebra.type) = (_ : FinRing.Ring.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : Num.ArchimedeanField.type) :> Type. +Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : Countable.type) :> Type. +Check erefl : (_ : Num.NumField.type) = (_ : Num.RealDomain.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : FinRing.Lmodule.type) :> Type. +Check erefl : (_ : GRing.Lmodule.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : CountRing.Field.type) = (_ : Countable.type) :> Type. +Check erefl : (_ : FinRing.Lalgebra.type) = (_ : Finite.type) :> Type. +Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : FinRing.ComRing.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : Countable.type) = (_ : FinRing.Lmodule.type) :> Type. +Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.Lalgebra.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.Field.type) :> Type. +Check erefl : (_ : GRing.Ring.type) = (_ : Num.NumDomain.type) :> Type. +Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.UnitRing.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : Num.ClosedField.type) :> Type. +Check erefl : (_ : FinRing.Algebra.type) = (_ : GRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : GRing.UnitAlgebra.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.Ring.type) :> Type. +Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : FinGroup.type) = (_ : FinRing.Lalgebra.type) :> Type. +Check erefl : (_ : GRing.ClosedField.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : CountRing.ComRing.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : GRing.ComRing.type) = (_ : Num.ArchimedeanField.type) :> Type. +Check erefl : (_ : GRing.Field.type) = (_ : Num.ArchimedeanField.type) :> Type. +Check erefl : (_ : GRing.Lalgebra.type) = (_ : Vector.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : Num.ClosedField.type) :> Type. +Check erefl : (_ : Countable.type) = (_ : FinGroup.type) :> Type. +Check erefl : (_ : GRing.UnitRing.type) = (_ : Num.RealField.type) :> Type. +Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : Finite.type) :> Type. +Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : Finite.type) :> Type. +Check erefl : (_ : GRing.Ring.type) = (_ : Num.RealDomain.type) :> Type. +Check erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.Lmodule.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : GRing.DecidableField.type) :> Type. +Check erefl : (_ : Countable.type) = (_ : FinRing.Field.type) :> Type. +Check erefl : (_ : FieldExt.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : CountRing.Field.type) = (_ : FinRing.ComUnitRing.type) :> Type. +Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : CountRing.ComRing.type) = (_ : Equality.type) :> Type. +Check erefl : (_ : FinGroup.type) = (_ : GRing.ComUnitRing.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : CountRing.UnitRing.type) :> Type. +Check erefl : (_ : FinGroup.type) = (_ : GRing.Field.type) :> Type. +Check erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.NumDomain.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : FinRing.UnitRing.type) :> Type. +Check erefl : (_ : FinRing.ComRing.type) = (_ : Finite.type) :> Type. +Check erefl : (_ : Countable.type) = (_ : GRing.ComUnitRing.type) :> Type. +Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.ComUnitRing.type) :> Type. +Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.DecidableField.type) :> Type. +Check erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.IntegralDomain.type) :> Type. +Check erefl : (_ : CountRing.Zmodule.type) = (_ : Countable.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : CountRing.Field.type) = (_ : FinRing.IntegralDomain.type) :> Type. +Check erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.UnitRing.type) :> Type. +Check erefl : (_ : CountRing.Zmodule.type) = (_ : Finite.type) :> Type. +Check erefl : (_ : GRing.Lmodule.type) = (_ : GRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : Finite.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.ClosedField.type) :> Type. +Check erefl : (_ : Finite.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : CountRing.UnitRing.type) = (_ : Equality.type) :> Type. +Check erefl : (_ : FinGroup.type) = (_ : FinRing.Field.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : Num.RealField.type) :> Type. +Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.Lalgebra.type) :> Type. +Check erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : FieldExt.type) :> Type. +Check erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.DecidableField.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : FieldExt.type) :> Type. +Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.Lmodule.type) :> Type. +Check erefl : (_ : GRing.DecidableField.type) = (_ : Num.NumDomain.type) :> Type. +Check erefl : (_ : GRing.DecidableField.type) = (_ : GRing.Field.type) :> Type. +Check erefl : (_ : CountRing.UnitRing.type) = (_ : Countable.type) :> Type. +Check erefl : (_ : FinRing.Lmodule.type) = (_ : FinRing.Ring.type) :> Type. +Check erefl : (_ : FieldExt.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : GRing.UnitAlgebra.type) = (_ : Vector.type) :> Type. +Check erefl : (_ : GRing.UnitRing.type) = (_ : Vector.type) :> Type. +Check erefl : (_ : FinRing.Lalgebra.type) = (_ : FinRing.Lmodule.type) :> Type. +Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.IntegralDomain.type) :> Type. +Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Ring.type) :> Type. +Check erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.RealClosedField.type) :> Type. +Check erefl : (_ : CountRing.Field.type) = (_ : FinRing.ComRing.type) :> Type. +Check erefl : (_ : GRing.IntegralDomain.type) = (_ : Vector.type) :> Type. +Check erefl : (_ : FinRing.Algebra.type) = (_ : GRing.Lmodule.type) :> Type. +Check erefl : (_ : GRing.Field.type) = (_ : GRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : Finite.type) :> Type. +Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.DecidableField.type) :> Type. +Check erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.Lalgebra.type) :> Type. +Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : Equality.type) :> Type. +Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.Field.type) :> Type. +Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : GRing.Field.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : CountRing.ComRing.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : FieldExt.type) = (_ : GRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : FinGroup.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : Num.RealClosedField.type) = (_ : Num.RealField.type) :> Type. +Check erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.Ring.type) :> Type. +Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.UnitRing.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : FinRing.Ring.type) :> Type. +Check erefl : (_ : FinGroup.type) = (_ : FinRing.Ring.type) :> Type. +Check erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.Ring.type) :> Type. +Check erefl : (_ : Countable.type) = (_ : FinRing.IntegralDomain.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : GRing.DecidableField.type) :> Type. +Check erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.ComRing.type) :> Type. +Check erefl : (_ : GRing.Ring.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : Num.RealDomain.type) = (_ : Num.RealField.type) :> Type. +Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.DecidableField.type) :> Type. +Check erefl : (_ : FinRing.ComRing.type) = (_ : GRing.Field.type) :> Type. +Check erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.ComRing.type) :> Type. +Check erefl : (_ : GRing.DecidableField.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinGroup.type) :> Type. +Check erefl : (_ : FinRing.Ring.type) = (_ : FinRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.Lmodule.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : FinRing.IntegralDomain.type) :> Type. +Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.ComRing.type) :> Type. +Check erefl : (_ : Falgebra.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : CountRing.ClosedField.type) :> Type. +Check erefl : (_ : Finite.type) = (_ : GRing.ComRing.type) :> Type. +Check erefl : (_ : GRing.ClosedField.type) = (_ : GRing.ComUnitRing.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : Equality.type) :> Type. +Check erefl : (_ : Falgebra.type) = (_ : GRing.Field.type) :> Type. +Check erefl : (_ : CountRing.DecidableField.type) = (_ : Equality.type) :> Type. +Check erefl : (_ : Countable.type) = (_ : GRing.Lmodule.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : Finite.type) :> Type. +Check erefl : (_ : FinRing.Field.type) = (_ : Finite.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.ClosedField.type) :> Type. +Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Zmodule.type) :> Type. +Check erefl : (_ : CountRing.UnitRing.type) = (_ : Finite.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : CountRing.DecidableField.type) :> Type. +Check erefl : (_ : Falgebra.type) = (_ : GRing.Algebra.type) :> Type. +Check erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.ComRing.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.ComRing.type) :> Type. +Check erefl : (_ : FinRing.Lmodule.type) = (_ : FinRing.Zmodule.type) :> Type. +Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : FinRing.IntegralDomain.type) :> Type. +Check erefl : (_ : CountRing.DecidableField.type) = (_ : CountRing.IntegralDomain.type) :> Type. +Check erefl : (_ : Countable.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : FinRing.Lmodule.type) = (_ : Finite.type) :> Type. +Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.IntegralDomain.type) :> Type. +Check erefl : (_ : CountRing.Field.type) = (_ : FinRing.Ring.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.ComRing.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : GRing.ComRing.type) :> Type. +Check erefl : (_ : GRing.ComRing.type) = (_ : Num.NumField.type) :> Type. +Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.ComUnitRing.type) :> Type. +Check erefl : (_ : FieldExt.type) = (_ : GRing.ComUnitRing.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : CountRing.ComRing.type) :> Type. +Check erefl : (_ : GRing.Field.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : GRing.Field.type) :> Type. +Check erefl : (_ : FinRing.Field.type) = (_ : FinRing.Zmodule.type) :> Type. +Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : FinRing.Zmodule.type) :> Type. +Check erefl : (_ : GRing.Ring.type) = (_ : Num.RealField.type) :> Type. +Check erefl : (_ : FieldExt.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : GRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : FinRing.UnitRing.type) :> Type. +Check erefl : (_ : GRing.UnitRing.type) = (_ : SplittingField.type) :> Type. +Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : FinGroup.type) = (_ : FinRing.Algebra.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : CountRing.UnitRing.type) :> Type. +Check erefl : (_ : Falgebra.type) = (_ : SplittingField.type) :> Type. +Check erefl : (_ : GRing.Lalgebra.type) = (_ : GRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : FieldExt.type) = (_ : GRing.Algebra.type) :> Type. +Check erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.ComRing.type) :> Type. +Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.ComRing.type) :> Type. +Check erefl : (_ : GRing.DecidableField.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : CountRing.Field.type) = (_ : GRing.ComRing.type) :> Type. +Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.Ring.type) :> Type. +Check erefl : (_ : Num.NumDomain.type) = (_ : Num.RealField.type) :> Type. +Check erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : CountRing.ClosedField.type) = (_ : Equality.type) :> Type. +Check erefl : (_ : Countable.type) = (_ : GRing.ClosedField.type) :> Type. +Check erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : Finite.type) = (_ : GRing.Lmodule.type) :> Type. +Check erefl : (_ : GRing.ComUnitRing.type) = (_ : Vector.type) :> Type. +Check erefl : (_ : GRing.ClosedField.type) = (_ : GRing.DecidableField.type) :> Type. +Check erefl : (_ : FinRing.ComRing.type) = (_ : GRing.ComUnitRing.type) :> Type. +Check erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.Field.type) :> Type. +Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : Equality.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : Num.RealField.type) :> Type. +Check erefl : (_ : Num.ClosedField.type) = (_ : Num.NumField.type) :> Type. +Check erefl : (_ : Num.NumDomain.type) = (_ : Num.RealDomain.type) :> Type. +Check erefl : (_ : FinRing.Field.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : CountRing.ComRing.type) = (_ : GRing.DecidableField.type) :> Type. +Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.Lmodule.type) :> Type. +Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.Field.type) :> Type. +Check erefl : (_ : CountRing.ComRing.type) = (_ : GRing.ComUnitRing.type) :> Type. +Check erefl : (_ : GRing.Lmodule.type) = (_ : SplittingField.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : FinRing.Field.type) :> Type. +Check erefl : (_ : Falgebra.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.DecidableField.type) :> Type. +Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.Zmodule.type) :> Type. +Check erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.UnitRing.type) :> Type. +Check erefl : (_ : FinRing.Field.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : GRing.Zmodule.type) = (_ : SplittingField.type) :> Type. +Check erefl : (_ : FinRing.Algebra.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : FinRing.Zmodule.type) :> Type. +Check erefl : (_ : GRing.UnitRing.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : FinRing.Algebra.type) :> Type. +Check erefl : (_ : GRing.Zmodule.type) = (_ : Num.RealClosedField.type) :> Type. +Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : GRing.Lalgebra.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : GRing.Ring.type) = (_ : Num.RealClosedField.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Field.type) :> Type. +Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : GRing.Ring.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Lalgebra.type) :> Type. +Check erefl : (_ : GRing.Field.type) = (_ : Num.ClosedField.type) :> Type. +Check erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.Zmodule.type) :> Type. +Check erefl : (_ : FinRing.Field.type) = (_ : GRing.ComRing.type) :> Type. +Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.Field.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : FinRing.Lalgebra.type) :> Type. +Check erefl : (_ : Num.ArchimedeanField.type) = (_ : Num.NumField.type) :> Type. +Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.ComUnitRing.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : Falgebra.type) :> Type. +Check erefl : (_ : GRing.Zmodule.type) = (_ : Num.RealDomain.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : Num.NumDomain.type) :> Type. +Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.Zmodule.type) :> Type. +Check erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.Algebra.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : GRing.Algebra.type) :> Type. +Check erefl : (_ : FinRing.Lmodule.type) = (_ : FinRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : Num.ArchimedeanField.type) = (_ : Num.RealDomain.type) :> Type. +Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.DecidableField.type) :> Type. +Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Algebra.type) :> Type. +Check erefl : (_ : GRing.Lmodule.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : FinGroup.type) = (_ : GRing.Lalgebra.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : FinRing.Lmodule.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : FinRing.ComUnitRing.type) :> Type. +Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : CountRing.Ring.type) :> Type. +Check erefl : (_ : GRing.UnitAlgebra.type) = (_ : SplittingField.type) :> Type. +Check erefl : (_ : Countable.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : Countable.type) = (_ : GRing.DecidableField.type) :> Type. +Check erefl : (_ : FieldExt.type) = (_ : GRing.Field.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : FinRing.Field.type) = (_ : GRing.ComUnitRing.type) :> Type. +Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.ComUnitRing.type) :> Type. +Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : GRing.Lalgebra.type) :> Type. +Check erefl : (_ : GRing.Algebra.type) = (_ : SplittingField.type) :> Type. +Check erefl : (_ : FinGroup.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : FinRing.Algebra.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : GRing.ComUnitRing.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Ring.type) :> Type. +Check erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.Lmodule.type) :> Type. +Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : CountRing.ComRing.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.ComRing.type) :> Type. +Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Lmodule.type) :> Type. +Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.ComUnitRing.type) :> Type. +Check erefl : (_ : GRing.ComRing.type) = (_ : Num.NumDomain.type) :> Type. +Check erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.Field.type) :> Type. +Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : FinRing.Zmodule.type) :> Type. +Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.Algebra.type) :> Type. +Check erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.ComUnitRing.type) :> Type. +Check erefl : (_ : CountRing.Field.type) = (_ : FinRing.UnitRing.type) :> Type. +Check erefl : (_ : Countable.type) = (_ : FinRing.ComRing.type) :> Type. +Check erefl : (_ : GRing.Field.type) = (_ : Vector.type) :> Type. +Check erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.ComUnitRing.type) :> Type. +Check erefl : (_ : GRing.Zmodule.type) = (_ : Num.RealField.type) :> Type. +Check erefl : (_ : GRing.Ring.type) = (_ : Num.NumField.type) :> Type. +Check erefl : (_ : GRing.ClosedField.type) = (_ : GRing.ComRing.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : Finite.type) = (_ : GRing.Field.type) :> Type. +Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Field.type) :> Type. +Check erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.Zmodule.type) :> Type. +Check erefl : (_ : FinRing.Field.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.ClosedField.type) :> Type. +Check erefl : (_ : Num.NumField.type) = (_ : Num.RealField.type) :> Type. +Check erefl : (_ : GRing.Ring.type) = (_ : Num.ArchimedeanField.type) :> Type. +Check erefl : (_ : GRing.UnitRing.type) = (_ : Num.RealDomain.type) :> Type. +Check erefl : (_ : FinGroup.type) = (_ : GRing.ComRing.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : FinGroup.type) :> Type. +Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.ComUnitRing.type) :> Type. +Check erefl : (_ : GRing.Ring.type) = (_ : Num.ClosedField.type) :> Type. +Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinGroup.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : FinRing.ComRing.type) :> Type. +Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.ComRing.type) :> Type. +Check erefl : (_ : GRing.Field.type) = (_ : Num.NumField.type) :> Type. +Check erefl : (_ : FinRing.Zmodule.type) = (_ : Finite.type) :> Type. +Check erefl : (_ : GRing.Zmodule.type) = (_ : Num.ClosedField.type) :> Type. +Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.ComRing.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.DecidableField.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : Equality.type) :> Type. +Check erefl : (_ : Falgebra.type) = (_ : FieldExt.type) :> Type. +Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.UnitRing.type) :> Type. +Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.ClosedField.type) :> Type. +Check erefl : (_ : GRing.Lmodule.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Field.type) :> Type. +Check erefl : (_ : GRing.Zmodule.type) = (_ : Num.NumField.type) :> Type. +Check erefl : (_ : Countable.type) = (_ : FinRing.ComUnitRing.type) :> Type. +Check erefl : (_ : CountRing.Field.type) = (_ : GRing.ComUnitRing.type) :> Type. +Check erefl : (_ : CountRing.Field.type) = (_ : CountRing.Ring.type) :> Type. +Check erefl : (_ : FieldExt.type) = (_ : GRing.Lalgebra.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : GRing.Lmodule.type) :> Type. +Check erefl : (_ : FinGroup.type) = (_ : FinRing.UnitRing.type) :> Type. +Check erefl : (_ : GRing.ComUnitRing.type) = (_ : SplittingField.type) :> Type. +Check erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.DecidableField.type) :> Type. +Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinGroup.type) :> Type. +Check erefl : (_ : CountRing.Field.type) = (_ : FinGroup.type) :> Type. +Check erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.Zmodule.type) :> Type. +Check erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.UnitRing.type) :> Type. +Check erefl : (_ : FinRing.Lmodule.type) = (_ : FinRing.UnitRing.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : GRing.Lmodule.type) :> Type. +Check erefl : (_ : GRing.Field.type) = (_ : Num.RealField.type) :> Type. +Check erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : GRing.UnitRing.type) = (_ : Num.RealClosedField.type) :> Type. +Check erefl : (_ : Finite.type) = (_ : GRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : Countable.type) = (_ : GRing.Field.type) :> Type. +Check erefl : (_ : GRing.UnitRing.type) = (_ : Num.ArchimedeanField.type) :> Type. +Check erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.Ring.type) :> Type. +Check erefl : (_ : FinRing.Algebra.type) = (_ : Finite.type) :> Type. +Check erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.NumDomain.type) :> Type. +Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.Field.type) :> Type. +Check erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.ArchimedeanField.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : CountRing.Ring.type) :> Type. +Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : Finite.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.ComUnitRing.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Lmodule.type) :> Type. +Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : CountRing.DecidableField.type) = (_ : CountRing.Ring.type) :> Type. +Check erefl : (_ : GRing.Lalgebra.type) = (_ : SplittingField.type) :> Type. +Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.ComRing.type) :> Type. +Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Field.type) :> Type. +Check erefl : (_ : GRing.DecidableField.type) = (_ : Num.NumField.type) :> Type. +Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : GRing.UnitRing.type) = (_ : Num.ClosedField.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : Finite.type) :> Type. +Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : Finite.type) :> Type. +Check erefl : (_ : FieldExt.type) = (_ : GRing.ComRing.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : Num.RealDomain.type) :> Type. +Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.Zmodule.type) :> Type. +Check erefl : (_ : Countable.type) = (_ : FinRing.Zmodule.type) :> Type. +Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : GRing.Field.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : CountRing.Field.type) = (_ : GRing.ClosedField.type) :> Type. +Check erefl : (_ : GRing.Field.type) = (_ : GRing.Lmodule.type) :> Type. +Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : FinRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : Falgebra.type) = (_ : GRing.Lmodule.type) :> Type. +Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : Finite.type) = (_ : GRing.Lalgebra.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.ComUnitRing.type) :> Type. +Check erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.RealField.type) :> Type. +Check erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.NumField.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : Num.NumField.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.IntegralDomain.type) :> Type. +Check erefl : (_ : CountRing.ComRing.type) = (_ : GRing.ComRing.type) :> Type. +Check erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.ClosedField.type) :> Type. +Check erefl : (_ : SplittingField.type) = (_ : Vector.type) :> Type. +Check erefl : (_ : Finite.type) = (_ : GRing.Algebra.type) :> Type. +Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : GRing.Field.type) = (_ : SplittingField.type) :> Type. +Check erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.IntegralDomain.type) :> Type. +Check erefl : (_ : CountRing.Field.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.UnitRing.type) :> Type. +Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : Countable.type) = (_ : FinRing.Ring.type) :> Type. +Check erefl : (_ : FinRing.UnitRing.type) = (_ : FinRing.Zmodule.type) :> Type. +Check erefl : (_ : FinRing.Ring.type) = (_ : FinRing.Zmodule.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : Num.NumField.type) :> Type. +Check erefl : (_ : GRing.ClosedField.type) = (_ : Num.NumField.type) :> Type. +Check erefl : (_ : GRing.ComRing.type) = (_ : SplittingField.type) :> Type. +Check erefl : (_ : GRing.ClosedField.type) = (_ : Num.NumDomain.type) :> Type. +Check erefl : (_ : GRing.ComRing.type) = (_ : Num.RealDomain.type) :> Type. +Check erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.ComUnitRing.type) :> Type. +Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.Lmodule.type) :> Type. +Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.RealField.type) :> Type. +Check erefl : (_ : Num.RealClosedField.type) = (_ : Num.RealDomain.type) :> Type. +Check erefl : (_ : Finite.type) = (_ : GRing.ComUnitRing.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : FinRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.ClosedField.type) :> Type. +Check erefl : (_ : FinGroup.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.RealClosedField.type) :> Type. +Check erefl : (_ : Finite.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : FieldExt.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : GRing.Field.type) = (_ : GRing.Lalgebra.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : FinRing.ComUnitRing.type) :> Type. +Check erefl : (_ : Countable.type) = (_ : GRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : CountRing.Field.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.IntegralDomain.type) :> Type. +Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.ClosedField.type) :> Type. +Check erefl : (_ : CountRing.Field.type) = (_ : GRing.Field.type) :> Type. +Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : GRing.ClosedField.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : Vector.type) :> Type. +Check erefl : (_ : GRing.Lalgebra.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.ComRing.type) :> Type. +Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : CountRing.Zmodule.type) :> Type. +Check erefl : (_ : FinRing.Ring.type) = (_ : FinRing.UnitRing.type) :> Type. +Check erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : Countable.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : CountRing.Zmodule.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : SplittingField.type) :> Type. +Check erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.Lalgebra.type) :> Type. +Check erefl : (_ : FinRing.ComRing.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : FinRing.Lalgebra.type) :> Type. +Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Field.type) :> Type. +Check erefl : (_ : GRing.DecidableField.type) = (_ : Num.ClosedField.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : CountRing.ComRing.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.ComUnitRing.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : GRing.ComRing.type) = (_ : Num.RealField.type) :> Type. +Check erefl : (_ : GRing.ClosedField.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.ComRing.type) :> Type. +Check erefl : (_ : Countable.type) = (_ : FinRing.UnitRing.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.ComRing.type) :> Type. +Check erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : SplittingField.type) :> Type. +Check erefl : (_ : Countable.type) = (_ : FinRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : CountRing.Field.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : GRing.Zmodule.type) = (_ : Vector.type) :> Type. +Check erefl : (_ : CountRing.Field.type) = (_ : CountRing.Zmodule.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : FinRing.Field.type) :> Type. +Check erefl : (_ : Falgebra.type) = (_ : GRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : FinRing.Algebra.type) = (_ : GRing.Algebra.type) :> Type. +Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.ComUnitRing.type) :> Type. +Check erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.Lalgebra.type) :> Type. +Check erefl : (_ : GRing.Zmodule.type) = (_ : Num.NumDomain.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.Algebra.type) :> Type. +Check erefl : (_ : FinGroup.type) = (_ : FinRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : Vector.type) :> Type. +Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.Field.type) :> Type. +Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : FinRing.Zmodule.type) :> Type. +Check erefl : (_ : Falgebra.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : Num.NumDomain.type) = (_ : Num.RealClosedField.type) :> Type. +Check erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : FinRing.UnitRing.type) :> Type. +Check erefl : (_ : CountRing.DecidableField.type) = (_ : CountRing.UnitRing.type) :> Type. +Check erefl : (_ : FinGroup.type) = (_ : FinRing.Lmodule.type) :> Type. +Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.UnitRing.type) :> Type. +Check erefl : (_ : FieldExt.type) = (_ : GRing.Lmodule.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : FinGroup.type) :> Type. +Check erefl : (_ : CountRing.ComRing.type) = (_ : GRing.Field.type) :> Type. +Check erefl : (_ : CountRing.Field.type) = (_ : Finite.type) :> Type. +Check erefl : (_ : FinGroup.type) = (_ : FinRing.ComUnitRing.type) :> Type. +Check erefl : (_ : GRing.Field.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : CountRing.Field.type) = (_ : CountRing.IntegralDomain.type) :> Type. +Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : Num.ArchimedeanField.type) = (_ : Num.RealField.type) :> Type. +Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.Algebra.type) :> Type. +Check erefl : (_ : Countable.type) = (_ : FinRing.Lalgebra.type) :> Type. +Check erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.Field.type) :> Type. +Check erefl : (_ : GRing.UnitAlgebra.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.Field.type) :> Type. +Check erefl : (_ : CountRing.Field.type) = (_ : FinRing.Field.type) :> Type. +Check erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.Lmodule.type) :> Type. +Check erefl : (_ : CountRing.Field.type) = (_ : CountRing.UnitRing.type) :> Type. +Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : GRing.ComRing.type) = (_ : Vector.type) :> Type. +Check erefl : (_ : CountRing.UnitRing.type) = (_ : CountRing.Zmodule.type) :> Type. +Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.IntegralDomain.type) :> Type. +Check erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.IntegralDomain.type) :> Type. +Check erefl : (_ : Countable.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : FinGroup.type) = (_ : GRing.Algebra.type) :> Type. +Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Zmodule.type) :> Type. +Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.Ring.type) :> Type. +Check erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.Lalgebra.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Lalgebra.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : GRing.Lalgebra.type) :> Type. +Check erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.ComUnitRing.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : Finite.type) :> Type. +Check erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.Lalgebra.type) :> Type. +Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Field.type) :> Type. +Check erefl : (_ : GRing.ClosedField.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : Countable.type) = (_ : GRing.Lalgebra.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : GRing.ComRing.type) :> Type. +Check erefl : (_ : CountRing.ComRing.type) = (_ : CountRing.ComUnitRing.type) :> Type. +Check erefl : (_ : CountRing.Field.type) = (_ : FinRing.Zmodule.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : Num.NumDomain.type) :> Type. +Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : FinRing.UnitRing.type) :> Type. +Check erefl : (_ : FinRing.UnitRing.type) = (_ : Finite.type) :> Type. +Check erefl : (_ : FinGroup.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : FinRing.Lalgebra.type) = (_ : FinRing.UnitRing.type) :> Type. +Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Lmodule.type) :> Type. +Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : FinRing.Field.type) :> Type. +Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Lmodule.type) :> Type. +Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinGroup.type) :> Type. +Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.UnitRing.type) :> Type. +Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.ComRing.type) :> Type. +Check erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Lalgebra.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : FinRing.IntegralDomain.type) :> Type. +Check erefl : (_ : GRing.DecidableField.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Field.type) :> Type. +Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : FinGroup.type) = (_ : FinRing.IntegralDomain.type) :> Type. +Check erefl : (_ : GRing.Ring.type) = (_ : Vector.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : FinRing.Algebra.type) :> Type. +Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : Finite.type) :> Type. +Check erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.DecidableField.type) :> Type. +Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : GRing.Field.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.Field.type) :> Type. +Check erefl : (_ : FinRing.Field.type) = (_ : GRing.Field.type) :> Type. +Check erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.Field.type) :> Type. +Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Ring.type) :> Type. +Check erefl : (_ : Num.ArchimedeanField.type) = (_ : Num.NumDomain.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : FinRing.Zmodule.type) :> Type. +Check erefl : (_ : Countable.type) = (_ : GRing.ComRing.type) :> Type. +Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.ComUnitRing.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : CountRing.IntegralDomain.type) :> Type. +Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : CountRing.Field.type) :> Type. +Check erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.Zmodule.type) :> Type. +Check erefl : (_ : CountRing.ClosedField.type) = (_ : Countable.type) :> Type. +Check erefl : (_ : CountRing.DecidableField.type) = (_ : CountRing.Field.type) :> Type. +Check erefl : (_ : CountRing.Field.type) = (_ : Equality.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : FinRing.ComRing.type) :> Type. +Check erefl : (_ : FinRing.Lmodule.type) = (_ : GRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : CountRing.Field.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : CountRing.Field.type) :> Type. +Check erefl : (_ : GRing.Field.type) = (_ : Num.RealClosedField.type) :> Type. +Check erefl : (_ : FinRing.Field.type) = (_ : FinRing.Ring.type) :> Type. +Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Lalgebra.type) :> Type. +Check erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.Ring.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : CountRing.ComUnitRing.type) :> Type. +Check erefl : (_ : FinRing.Field.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Algebra.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : CountRing.Zmodule.type) :> Type. +Check erefl : (_ : CountRing.DecidableField.type) = (_ : Countable.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : Countable.type) :> Type. +Check erefl : (_ : CountRing.DecidableField.type) = (_ : CountRing.Zmodule.type) :> Type. +Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : FinRing.Ring.type) :> Type. +Check erefl : (_ : FinGroup.type) = (_ : FinRing.ComRing.type) :> Type. +Check erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : FinRing.IntegralDomain.type) = (_ : GRing.ComRing.type) :> Type. +Check erefl : (_ : Falgebra.type) = (_ : GRing.ComUnitRing.type) :> Type. +Check erefl : (_ : FinRing.Lalgebra.type) = (_ : FinRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.Lalgebra.type) :> Type. +Check erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.Zmodule.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.Lmodule.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.ComUnitRing.type) :> Type. +Check erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.ComUnitRing.type) :> Type. +Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.ClosedField.type) :> Type. +Check erefl : (_ : GRing.Lalgebra.type) = (_ : GRing.Lmodule.type) :> Type. +Check erefl : (_ : FinRing.Ring.type) = (_ : GRing.Lalgebra.type) :> Type. +Check erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.Field.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Zmodule.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Algebra.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : GRing.ComUnitRing.type) :> Type. +Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : Countable.type) :> Type. +Check erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.RealDomain.type) :> Type. +Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.DecidableField.type) :> Type. +Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.ComUnitRing.type) :> Type. +Check erefl : (_ : GRing.UnitRing.type) = (_ : Num.NumField.type) :> Type. +Check erefl : (_ : GRing.DecidableField.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : GRing.ClosedField.type) = (_ : Num.ClosedField.type) :> Type. +Check erefl : (_ : GRing.Algebra.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.ComRing.type) :> Type. +Check erefl : (_ : FinGroup.type) = (_ : Finite.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : FinRing.UnitRing.type) :> Type. +Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.Algebra.type) :> Type. +Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Lalgebra.type) :> Type. +Check erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.Algebra.type) :> Type. +Check erefl : (_ : FinRing.Ring.type) = (_ : Finite.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : Num.RealDomain.type) :> Type. +Check erefl : (_ : Falgebra.type) = (_ : GRing.ComRing.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : GRing.Algebra.type) :> Type. +Check erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.ComUnitRing.type) :> Type. +Check erefl : (_ : GRing.ComRing.type) = (_ : Num.RealClosedField.type) :> Type. +Check erefl : (_ : GRing.IntegralDomain.type) = (_ : SplittingField.type) :> Type. +Check erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : Falgebra.type) = (_ : GRing.Lalgebra.type) :> Type. +Check erefl : (_ : GRing.IntegralDomain.type) = (_ : Num.NumField.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : Falgebra.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : FinRing.ComRing.type) = (_ : FinRing.ComUnitRing.type) :> Type. +Check erefl : (_ : CountRing.Zmodule.type) = (_ : GRing.ComUnitRing.type) :> Type. +Check erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : CountRing.ComRing.type) = (_ : GRing.ClosedField.type) :> Type. +Check erefl : (_ : GRing.ComRing.type) = (_ : Num.ClosedField.type) :> Type. +Check erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.Field.type) :> Type. +Check erefl : (_ : Countable.type) = (_ : Finite.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : FinRing.Lmodule.type) :> Type. +Check erefl : (_ : FinRing.Lalgebra.type) = (_ : FinRing.Zmodule.type) :> Type. +Check erefl : (_ : GRing.Lalgebra.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : GRing.UnitRing.type) = (_ : Num.NumDomain.type) :> Type. +Check erefl : (_ : FinRing.UnitRing.type) = (_ : GRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.Field.type) :> Type. +Check erefl : (_ : Num.ClosedField.type) = (_ : Num.NumDomain.type) :> Type. +Check erefl : (_ : FinRing.Field.type) = (_ : FinRing.IntegralDomain.type) :> Type. +Check erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.ArchimedeanField.type) :> Type. +Check erefl : (_ : CountRing.Zmodule.type) = (_ : Equality.type) :> Type. +Check erefl : (_ : Falgebra.type) = (_ : Vector.type) :> Type. +Check erefl : (_ : GRing.Lmodule.type) = (_ : Vector.type) :> Type. +Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : CountRing.UnitRing.type) :> Type. +Check erefl : (_ : FinRing.Field.type) = (_ : FinRing.UnitRing.type) :> Type. +Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : FinRing.ComRing.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : GRing.Ring.type) = (_ : SplittingField.type) :> Type. +Check erefl : (_ : FinRing.Zmodule.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : FinGroup.type) = (_ : GRing.Lmodule.type) :> Type. +Check erefl : (_ : CountRing.Field.type) = (_ : GRing.DecidableField.type) :> Type. +Check erefl : (_ : CountRing.ComRing.type) = (_ : Countable.type) :> Type. +Check erefl : (_ : FinGroup.type) = (_ : FinRing.Zmodule.type) :> Type. +Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.UnitRing.type) :> Type. +Check erefl : (_ : GRing.ClosedField.type) = (_ : GRing.Field.type) :> Type. +Check erefl : (_ : Num.NumDomain.type) = (_ : Num.NumField.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : FinRing.Ring.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : Num.ArchimedeanField.type) :> Type. +Check erefl : (_ : FinGroup.type) = (_ : GRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : CountRing.ClosedField.type) = (_ : GRing.Field.type) :> Type. +Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.IntegralDomain.type) :> Type. +Check erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.DecidableField.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : FinRing.UnitAlgebra.type) = (_ : GRing.Lalgebra.type) :> Type. +Check erefl : (_ : FinRing.ComRing.type) = (_ : GRing.ComRing.type) :> Type. +Check erefl : (_ : Falgebra.type) = (_ : GRing.IntegralDomain.type) :> Type. +Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : GRing.ClosedField.type) :> Type. +Check erefl : (_ : FieldExt.type) = (_ : Vector.type) :> Type. +Check erefl : (_ : CountRing.DecidableField.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : CountRing.ComRing.type) = (_ : Finite.type) :> Type. +Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.Zmodule.type) :> Type. +Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : GRing.DecidableField.type) :> Type. +Check erefl : (_ : CountRing.Ring.type) = (_ : FinGroup.type) :> Type. +Check erefl : (_ : Equality.type) = (_ : Num.RealClosedField.type) :> Type. +Check erefl : (_ : GRing.Algebra.type) = (_ : Vector.type) :> Type. +Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : FinRing.ComRing.type) :> Type. +Check erefl : (_ : GRing.ComRing.type) = (_ : GRing.ComUnitRing.type) :> Type. +Check erefl : (_ : FinRing.ComUnitRing.type) = (_ : FinRing.Ring.type) :> Type. +Check erefl : (_ : GRing.Ring.type) = (_ : GRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : CountRing.ComUnitRing.type) = (_ : FinRing.Ring.type) :> Type. +Check erefl : (_ : GRing.IntegralDomain.type) = (_ : GRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : CountRing.IntegralDomain.type) = (_ : GRing.ClosedField.type) :> Type. +Check erefl : (_ : FinRing.Algebra.type) = (_ : FinRing.Lmodule.type) :> Type. +Check erefl : (_ : Countable.type) = (_ : GRing.Algebra.type) :> Type. +Check erefl : (_ : FinRing.Algebra.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : GRing.ComUnitRing.type) = (_ : Num.RealDomain.type) :> Type. +Check erefl : (_ : Countable.type) = (_ : FinRing.Algebra.type) :> Type. +Check erefl : (_ : FinRing.Algebra.type) = (_ : GRing.Lalgebra.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : Num.RealClosedField.type) :> Type. +Check erefl : (_ : Countable.type) = (_ : Equality.type) :> Type. +Check erefl : (_ : FinRing.Lalgebra.type) = (_ : GRing.Lmodule.type) :> Type. +Check erefl : (_ : FinRing.ComRing.type) = (_ : GRing.UnitRing.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : GRing.ClosedField.type) :> Type. +Check erefl : (_ : Countable.type) = (_ : GRing.Ring.type) :> Type. +Check erefl : (_ : Choice.type) = (_ : GRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : GRing.ComUnitRing.type) = (_ : GRing.UnitAlgebra.type) :> Type. +Check erefl : (_ : GRing.Zmodule.type) = (_ : Num.ArchimedeanField.type) :> Type. + +(* fix in ssrnum *) +Fail Check erefl : (_ : GRing.Field.type) = (_ : Num.NumDomain.type) :> Type. +Fail Check erefl : (_ : GRing.Field.type) = (_ : Num.RealDomain.type) :> Type. + +(* fix in countalg *) +Fail Check erefl : (_ : CountRing.ClosedField.type) = (_ : CountRing.IntegralDomain.type) :> Type. +Fail Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Lmodule.type) :> Type. +Fail Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Algebra.type) :> Type. +Fail Check erefl : (_ : CountRing.UnitRing.type) = (_ : GRing.Lalgebra.type) :> Type. + +(* fix in finalg *) +Fail Check erefl : (_ : CountRing.Zmodule.type) = (_ : FinRing.Algebra.type) :> Type. +Fail Check erefl : (_ : CountRing.ComRing.type) = (_ : FinRing.UnitRing.type) :> Type. +Fail Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Algebra.type) :> Type. +Fail Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Lalgebra.type) :> Type. +Fail Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.Lmodule.type) :> Type. +Fail Check erefl : (_ : CountRing.UnitRing.type) = (_ : FinRing.ComRing.type) :> Type. -- cgit v1.2.3