Karl Palmskog (Sep 07 2021 at 16:34): Karl Palmskog (Sep 07 2021 at 16:34):Thanks to porting work by Yves Bertot, the development by Guillaume Cano from 2014 on normal forms for matrices (building towards Perron-Frobenius) is now compatible with MC 1.12.0 and beyond and has found a home in coq-community: https://github.com/coq-community/matrix_canonical_forms
Karl Palmskog (Sep 07 2021 at 16:37):since this a relatively small repo (~2500 LOC), it may be worth considering incorporating this code into a larger MC-based repo, e.g., CoqEAL
Pierre Roux (Sep 07 2021 at 17:44):If it builds on CoqEAL, that could indeed make sense.
Karl Palmskog (Sep 07 2021 at 18:05):yeah, it's highly dependent on CoqEAL. The main "cost" to CoqEAL would be introducing a dependency on mathcomp-real-closed
Last updated: Feb 08 2023 at 04:04 UTC