Stream: Beginner Questions

Topic: closure_of


view this post on Zulip 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...

view this post on Zulip 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_

view this post on Zulip 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

view this post on Zulip Jakub Kądziołka (Jun 30 2021 at 12:36):

It is an infix operator, so you probably want closedin Ta (Ta closure_of A)

view this post on Zulip Nicolò Cavalleri (Jun 30 2021 at 15:09):

Oh I see I didn't know what infix meant then! Thanks!


Last updated: Aug 15 2022 at 04:16 UTC