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...
'_ means that it's a literal
_ and not a parameter like in
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)
Oh I see I didn't know what infix meant then! Thanks!
Last updated: Aug 15 2022 at 04:16 UTC