[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 =
assumes "order<=base\<times>base" and "refl(base,order)" and "antisym(order)" and "trans(order)"
locale dual = poset "base" "converse(order)"
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