Stream: Beginner Questions

Topic: import quotes


view this post on Zulip zibo yang (Apr 13 2021 at 09:21):

Hi guys, can anyone explain about what is the difference between imports "geometry_theory" and imports geometry_theory. What is the meaning of using quotation mark here?

view this post on Zulip Mathias Fleury (Apr 13 2021 at 09:23):

No difference.

view this post on Zulip Jakub Kądziołka (Apr 13 2021 at 09:24):

sometimes the quotes are necessary if the theory you're importing contains some special characters, such as -

view this post on Zulip Mathias Fleury (Apr 13 2021 at 09:24):

However you need the quotations marks if the name contains an hyphen, like "HOL-Library.<theory>"

view this post on Zulip Mathias Fleury (Apr 13 2021 at 09:27):

(Also, the Isabelle convention is to capitalise theory names like Geometry_Theory)

view this post on Zulip zibo yang (Apr 13 2021 at 09:30):

you are right


Last updated: Mar 29 2024 at 12:28 UTC