[isabelle] When to expect working duals with locales?



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?

-- 
Victor Porton - http://portonvictor.org





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.