zibo yang (Apr 13 2021 at 09:21): 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?
Mathias Fleury (Apr 13 2021 at 09:23):No difference.
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 -
Mathias Fleury (Apr 13 2021 at 09:24):However you need the quotations marks if the name contains an hyphen, like "HOL-Library.<theory>"
Mathias Fleury (Apr 13 2021 at 09:27):(Also, the Isabelle convention is to capitalise theory names like Geometry_Theory)
zibo yang (Apr 13 2021 at 09:30):you are right
Last updated: Dec 21 2024 at 16:20 UTC