Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] When to expect working duals with locales?

view this post on Zulip Email Gateway (Aug 18 2022 at 16:55):

From: Victor Porton <porton@narod.ru>
Hi Larry Paulson, Tobias Nipkow, and Makarius Wenzel,

Remember I requested the feature to in some way allow definition of locales for dual posets and dual lattices?

I also suggested that this can be implemented as nested locales that is locales, that is locale definitions inside locales:

locale poset =
fixes base::i
fixes order::i
assumes "order<=base\<times>base" and "refl(base,order)" and "antisym(order)" and "trans(order)"
begin
locale dual = poset "base" "converse(order)"
end

When we can expect that this will be implemented? Is it worth to wait? For me Isabelle is completely unusable without this feature. I ask: How long to wait for these things to work properly?

Last updated: Apr 23 2024 at 12:29 UTC