Email Gateway (Aug 22 2022 at 16:55): Email Gateway (Aug 22 2022 at 16:55):From: Sebastien Gouezel <sebastien.gouezel@univ-nantes.fr>
When using HOL-Analysis, Min refers by default to linorder_class.Min.
However, when I import "HOL-Decision_Procs.Approximation", then Min
refers now to floatarith.Min, and I have to replace all my uses of Min
by linorder_class.Min to get everything straight.
What would be the best way to hide floatarith.Min so that Min still
refers to linorder_class.Min? (What I would like to do is import
Approximation in its own namespace, for instance.)
Sebastien
Email Gateway (Aug 22 2022 at 16:55):From: Manuel Eberl <eberlm@in.tum.de>
You can do a "hide_const (open) Approximation.Min". Then "Min" refers to
the "normal" Min as intended and one has to refer to the one from
Approximation with its full name. Except one doesn't really have to do
that anyway because it's more of an internal constant anyway.
This is a known issue. I think Fabian Immler is currently cleaning up
and modernising the Approximation package anyway, and in the same vein,
these problems will probably be solved properly when he is done.
Manuel
Email Gateway (Aug 22 2022 at 16:55):From: Sebastien Gouezel <sebastien.gouezel@univ-nantes.fr>
Thanks!
Last updated: Nov 21 2024 at 12:39 UTC