Philipp G. Haselwarter (Nov 08 2021 at 10:18): Philipp G. Haselwarter (Nov 08 2021 at 10:18):I do have a question for here rather than the issue tracker though -- what's a reasonable way to go about automating these simple minded fset proofs?
Karl Palmskog (Nov 08 2021 at 10:19):hmm, isn't fset MathComp stuff? Then I would look into ssrAC: https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrAC.v
Théo Winterhalter (Nov 08 2021 at 10:23):Here it is the fset from extructures. And ssrAC does not provide any automation does it?
Théo Winterhalter (Nov 08 2021 at 10:23):Can be interesting nonetheless indeed.
Karl Palmskog (Nov 08 2021 at 10:24):my understanding of ssrAC is that you get rewriting modulo AC with the regular SSR rewrite, but I could be wrong
Théo Winterhalter (Nov 08 2021 at 10:30):The file you gave says:
Rewriting with AC (not modulo AC), using a small scale command.
Philipp G. Haselwarter (Nov 08 2021 at 10:43):thanks for the pointer!
Last updated: Oct 13 2024 at 01:02 UTC