Lucie Lahaye

Add support for deriving simple instances for mutually inductive types.

1

This pull request adds partial support for deriving instances of mutually inductive types. Only limited to simple typeclasses. The supported typeclasses are: - GenSized - EnumSized - Shrink - Arbitrary...

`forAllShrinkNonDet` acts no different than `forAllShrink`

2

As far as I know, `forAllShrinkNonDet` is not documented anywhere. Reading its source code, I think it's supposed to be an alternative to `forAllShrink` to use when the property to...

realType structure over fourcolor's reals

1

During an internship with @CohenCyril, I worked on proving the equivalence between math-comp's realType and fourcolor's Real.model. The original idea was to transfer [Fourcolor](https://github.com/rocq-community/fourcolor)'s proof of categoricity for their reals...

Add warning about implicitly local `HB.instance` calls, improve error messages

2

For more context, see the [corresponding topic](https://rocq-prover.zulipchat.com/#narrow/channel/237868-Hierarchy-Builder-devs-.26-users/topic/Instanciating.20a.20mixin.20on.20a.20derived.20type.20when.20using.20a.20factory/with/544807859) on Zulip. Demo: ```coq From HB Require Import structures. HB.mixin Record Mixin T := {}. HB.structure Definition _ := { T of Mixin...