affeldt-aist

issue when loading mathcomp/HB

8

Hi, I am just forwarding an issue identified @Zimmi48 that I seem to have run into when testing alectryon. It seems to be an issue that arises by just loading...

help understanding sertop error

1

The following file `test.v`: ``` From mathcomp Require Import all_ssreflect. From HB Require Import structures. ``` compiled with the following command: `alectryon --frontend coq+rst --backend webpage test.v` fails with the...

move nsatz to MathComp -Analysis?

1

There is an instance of nsatz with rcfType in https://github.com/affeldt-aist/coq-robot/blob/master/ssr_ext.v Similarly, there is an instance of nsatz with realType in https://github.com/math-comp/analysis/pull/383 Should the rcfType instance of nsatz move in Analysis...

https://github.com/affeldt-aist/coq-robot/blob/ce7c75a7a2a990c446735299ad9ca04e8f621ebd/ssr_ext.v#L116-L121 this requires to first declare a numDomainType structure for matrices

fyi: @thery

https://github.com/affeldt-aist/infotheo/blob/56a667c1421a9eb7a62593512a609711c0938f4f/lib/ssrR.v#L79 @t6s @garrigue

prob interface

2

https://github.com/affeldt-aist/infotheo/blob/fdba7c47f758c2276c30b78bc35f69a279871527/lib/Reals_ext.v#L387 Since we're favoring a structure with an inequality in `bool` for `prob`, the constructor `mk_` might turn out to be superfluous after all. Investigate its removal. Cc: @t6s

vandermonde to MathComp

3

https://github.com/affeldt-aist/infotheo/blob/56a667c1421a9eb7a62593512a609711c0938f4f/lib/vandermonde.v#L8 this should be cleaned and PRed to MathComp...

(turned into draft PR for visibility)