Email Gateway (Aug 18 2022 at 14:54): Email Gateway (Aug 18 2022 at 14:54):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Viorel,
you have to import theory Lattice_Syntax to obtain pretty syntax for the
lattice operations.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 14:54):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello,
I am trying to use the symbol \<sqinter> instead of inf. However I get
the error
message Inner lexical error at: \<sqinter> ...
If I use (inf S T) instead of (S \<sqinter> T) everything works OK.
Best regards,
Viorel Preoteasa
Email Gateway (Aug 18 2022 at 14:54):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Viorel,
in the HOL theorie the lattice syntax is deleted ("no_notation") at the
end of each lattice section. Once there was a fundamental decision not
to enrich the syntax universe of the HOL theories any more, in order
that users stay free to use it after their fashion. This of course does
not solve the fundamental problem of how to control syntax
appropriately, but it is a usable compromise.
Hope this helps
Florian
signature.asc
Last updated: Apr 20 2024 at 04:19 UTC