Re: [isabelle] Min shadowing

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.


On 10/03/18 15:04, Sebastien Gouezel wrote:
> 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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.