Bas Spitters (Jun 01 2023 at 12:46): Bas Spitters (Jun 01 2023 at 12:46):I seem to recall that algebra tactics also work for stdlib rings/fields. However, rereading the documentation, this does not seem to be the case.
Am I misremembering? Is there another standard solution?
https://github.com/math-comp/algebra-tactics
Pierre Roux (Jun 01 2023 at 12:50):I'm not sure I understand the question, algebra-tactics is for matchomp not for stdlib. You can still equip the stdlib types with mathcomp structures to get some compatibility but otherwise I don't think it's expected to work out of the box (some of these structures, for Z, may already exist in mczify though).
Kazuhiko Sakaguchi (Jun 01 2023 at 14:35):At least ring and field of Algebra Tactics provide a special treatment for Z: https://github.com/math-comp/algebra-tactics/blob/master/theories/ring.elpi#L205 (If you read the paper, I guess this is what you "misremember.")
Kazuhiko Sakaguchi (Jun 01 2023 at 14:38):You can embed Z to any ring through the int_of_Z morphism and _%:~R. Algebra Tactics can recognize these morphisms.
Bas Spitters (Jun 02 2023 at 07:22):Thanks. Yes, I was thinking of some mczify type of preprocessing.
Last updated: Oct 13 2024 at 01:02 UTC