Stream: Beginner Questions

Topic: How to deal with name shadowing?


view this post on Zulip Jakub Kądziołka (Jan 16 2021 at 20:18):

There are two definitions for prime - one in HOL-Computational_Algebra.Factorial_Ring, and one in HOL-Algebra.Divisibility. When I import both HOL-Number_Theory and HOL-Algebra into a theory (regardless of the order), the latter shadows the former. Thus, if I want to refer to primality of integers, I need to use the full Factorial_Ring.prime. What's the best way to instruct Isabelle to default to Factorial_Ring.prime in my theory?

view this post on Zulip Manuel Eberl (Jan 16 2021 at 21:08):

no idea if there is one

view this post on Zulip Manuel Eberl (Jan 16 2021 at 21:09):

that is a long-standing problem with a number of things

view this post on Zulip Manuel Eberl (Jan 16 2021 at 21:09):

I guess you can do hide_const (open) Divisibility.prime

view this post on Zulip Manuel Eberl (Jan 16 2021 at 21:10):

then you have to spell out Divisibility.prime whenever you want to refer to that

view this post on Zulip Jakub Kądziołka (Jan 16 2021 at 23:01):

Ah, thanks. That's satisfactory to me, as I'm not using Divisibility.prime in particular


Last updated: Sep 25 2021 at 10:20 UTC