Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Instatiating locales: where is the error?

Email Gateway (Aug 18 2022 at 16:35):

From: Victor Porton <porton@narod.ru>
theory test
imports Main_ZF
begin

locale t =
fixes "x"
assumes "x=0"
begin
end

locale q = t "1"

end

How the locale q is instantiated without proof that "x=0" (in fact x is non-zero but instead "x=1"). I understand something about locales wrongly. Where is the error? How to obtain an instance of a locale?

Last updated: May 06 2024 at 16:21 UTC