Stream: Hierarchy Builder devs & users

Topic: Importing Order.TTheory in the middle break the code


view this post on Zulip Florent Hivert (Dec 11 2023 at 12:56):

The following code

From HB Require Import structures.
From mathcomp Require Import all_ssreflect.

Structure foo : Type := Foo {fooval :> seq nat; _ : size fooval == 1}.
HB.instance Definition _ := [isSub of foo for fooval].
HB.instance Definition _ := [Equality of foo by <:].

Import Order.TTheory.   (* HERE *)

Structure bar : Type := Bar {barval :> seq nat; _ : size barval == 0}.
HB.instance Definition _ := [isSub of bar for barval].
HB.instance Definition _ := [Equality of bar by <:].

Fails on the last line with

 Error: eqtype_Equality__to__eqtype_hasDecEq already exists.

On the other hand, if the import of Order.TTheory is before the declaration of foo or not here at all, everything works.
Is this expected ?


Last updated: Apr 21 2024 at 01:02 UTC