Re: [isabelle] Min shadowing
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Min shadowing
- From: Manuel Eberl <eberlm at in.tum.de>
- Date: Sat, 10 Mar 2018 15:15:06 +0100
- In-reply-to: <firstname.lastname@example.org>
- References: <email@example.com>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.6.0
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.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and