Hi, I was playing with preorders using HB:

```
HB.mixin
Record PreOrder_of_Type A := {
ord : rel A;
ord_refl : reflexive ord;
ord_trans : transitive ord }.
HB.structure
Definition PreOrder := { A of PreOrder_of_Type A }.
```

Now I want to add another mixin to get partial orders, e.g.,

```
HB.mixin
Record Order_of_PreOrder A of PreOrder A := {
ord_anti : antisymmetric (@ord A)
}.
```

but of course, this doesn't work, as `ord`

expects a `PreOrder.type`

while here, `A`

is just a `Type`

. What's the idiomatic way to deal with this?

I think in dioid I just wrote something like `@antisymmetric A ord`

Agree.

But I wonder what happens if `antisymmetric`

is a notation.

Then maybe something like `@ord (PreOrder.clone A _)`

(haven't tried though)

Xavier Allamigeon said:

but of course, this doesn't work, as

`ord`

expects a`PreOrder.type`

while here,`A`

is just a`Type`

. What's the idiomatic way to deal with this?

You can use `[the PreOrder.type of A]`

Pierre Roux said:

Then maybe something like

`@ord (PreOrder.clone A _)`

(haven't tried though)

This should work as well.

IMO a type annotation is simpler. HB will put on `A`

a canonical `PreOrder`

before typing the mixin fields, but the missing piece of info is that you talk about `A`

when you mention `ord`

:

```
From HB Require Import structures.
From Coq Require Import ssreflect ssrfun ssrbool ZArith.
HB.mixin
Record PreOrder_of_Type A := {
ord : rel A;
ord_refl : reflexive ord;
ord_trans : transitive ord }.
HB.structure
Definition PreOrder := { A of PreOrder_of_Type A }.
HB.mixin
Record Order_of_PreOrder A of PreOrder A := {
ord_anti : antisymmetric (ord : A -> _)
}.
```

Maybe `(ord : rel A)`

would be more polite in this specific case

These phenomena are quite recurrent in our demos, we should probably write an FAQ

Last updated: Oct 13 2024 at 01:02 UTC