Nicolò Cavalleri (Jun 30 2021 at 11:42): Nicolò Cavalleri (Jun 30 2021 at 11:42):I cannot manage to use closure_of outside of the file Abstract_topology. If I use it in another file that imports it, it gets colored in light blue and the following error is given:
Inner syntax error⌂
Failed to parse prop
I see that next to its definition there is written (infixr "closure'_of" 80), but if I try to use closure'_of instead, isabelle does not recognize it as anythig and treats it as a free variable. Does anyone know what the problem might be? All other definitions from that file work fine...
Jakub Kądziołka (Jun 30 2021 at 11:51):the '_ means that it's a literal _ and not a parameter like in if_then_else_
Nicolò Cavalleri (Jun 30 2021 at 12:30):Do you then know what I am doing wrong? This is a mwe in case it's needed:
theory Scratch
imports "HOL-Analysis.Abstract_topology"
begin
lemma foo: "closedin Ta (closure_of Ta A)"
end
It is an infix operator, so you probably want closedin Ta (Ta closure_of A)
Nicolò Cavalleri (Jun 30 2021 at 15:09):Oh I see I didn't know what infix meant then! Thanks!
Last updated: Dec 21 2024 at 16:20 UTC