Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Min shadowing


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Email Gateway (Aug 22 2022 at 16:55):

From: Sebastien Gouezel <sebastien.gouezel@univ-nantes.fr>
Thanks!


Last updated: Mar 29 2024 at 04:18 UTC