Email Gateway (Aug 19 2022 at 16:12): Email Gateway (Aug 19 2022 at 16:12):From: M A <tesleft@hotmail.com>
Hi
expect to unifying theory Lists and Lattices, is lists the correct collection for implementing lattices, if not, which theory for this
when extract all circus code
C:\Users\martlee2\Downloads\Isabelle\Isabelle2014\src\Designs.thy
in src directory
this time error become
Bad theory (file "C:\Users\martlee2\Downloads\Isabelle\Isabelle2014\src\Lists.thy")
theory testlattice
imports Designs Relations Lists Lattices
begin
end
Regards,
Martin
Email Gateway (Aug 19 2022 at 16:12):From: M A <tesleft@hotmail.com>
Hi
C:\Users\martlee2\Downloads\Isabelle\Isabelle2014\src\HOL\Circus
Bad theory (file "C:\Users\marin\Downloads\Isabelle\Isabelle2014\src\Circus.thy")
Regards,
Martin
Email Gateway (Aug 19 2022 at 16:12):From: Lawrence Paulson <lp15@cam.ac.uk>
There is no need to combine theories in this way. The theory Main contains everything you need.
I urge you to work through the tutorials. They are the first two items listed on the documentation page
http://www.cl.cam.ac.uk/research/hvg/Isabelle/documentation.html
You need to understand the basics before you can try anything advanced.
Larry Paulson
Email Gateway (Aug 19 2022 at 16:12):From: M A <tesleft@hotmail.com>
Hi
I use Main got error, how to make meet or join in expression of list?
Outer syntax error⌂: keyword "=" expected,
but identifier list⌂ was found
theory testlattice
imports Main
begin
datatype meetlist list = Nil | Cons meet_commute |
end
Regards,
Martin
Last updated: Apr 18 2024 at 12:27 UTC