Craig Alan Feinstein (Aug 28 2024 at 21:29): Craig Alan Feinstein (Aug 28 2024 at 21:29):I'm getting a warning for ambiguous parsing of the equation:
"(lagrange_trans_of_4((a, b, c, d),(w, x, y, z))$ 0)^2 +
(lagrange_trans_of_4((a, b, c, d),(w, x, y, z))$ 1)^2 +
(lagrange_trans_of_4((a, b, c, d),(w, x, y, z))$ 2)^2 +
(lagrange_trans_of_4((a, b, c, d),(w, x, y, z))$ 3)^2 =
(of_nat n) * (w^2 + x^2 + y^2 + z^2)"
It says, "Fortunately, only one parse tree is well-formed and type-correct,
but you may still want to disambiguate your grammar or your input."
Why would it even have problems with this, as it seems to me to be pretty easy to parse?
Craig Alan Feinstein (Aug 28 2024 at 22:36):I looked at two of the 16 parse trees and got the following differences:
("\<^const>HOL.Trueprop"
("\<^const>HOL.eq"
("\<^const>Groups.plus_class.plus"
("\<^const>Groups.plus_class.plus"
("\<^const>Groups.plus_class.plus"
("\<^const>Power.power_class.power"
("\<^const>Formal_Power_Series.fps.fps_nth"
("\<^const>HOL.Trueprop"
("\<^const>HOL.eq"
("\<^const>Groups.plus_class.plus"
("\<^const>Groups.plus_class.plus"
("\<^const>Groups.plus_class.plus"
("\<^const>Power.power_class.power"
("\<^const>Matrix.vec_index"
So I guess the Matrix.vec_index library interprets it one way while Formal_Power_Series.fps.fps_nth interprets it another?
Craig Alan Feinstein (Aug 29 2024 at 00:22):A question is is it better to ignore this or is there a more fundamental problem with something I'm doing?
Mathias Fleury (Aug 29 2024 at 05:01):Normally I would say ignore. But here it might lead to some very strange typing issues or stuff that looks right but is interpreted wrong. So if you are sure to not use the FPS, you can also hide the notation (with no_notation)
Mathias Fleury (Aug 29 2024 at 05:04):(no_notation has some very interesting consequences in the order of the imports for later imports as notation merges are done in a certain order)
Craig Alan Feinstein (Aug 29 2024 at 19:10):Yesterday after I posted, I changed lagrange_trans_of_4 to a 4 by 1 matrix instead of a 4 dimensional vector and it didn’t give me a warning. Is this a better format than no_notation?
Last updated: Dec 21 2024 at 16:20 UTC