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
Robert Soeldner (Dec 13 2021 at 20:01):Hi,
shouldn't the goal be solved directly by the two assumptions?
I struggle understanding the current "problem" :-)
using this:
?x ∈ E ⟹ t ?x = Some ?y ⟶ ?y ∈ V
?x ∉ E ⟹ t ?x = None
goal (1 subgoal):
1. ran t = V
Last updated: Jul 15 2022 at 23:21 UTC