Seung Hoon Park (Mar 18 2022 at 20:05): Seung Hoon Park (Mar 18 2022 at 20:05):I'm looking at the 'Haskell-style type classes with Isabelle/Isar' tutorial available online in the Isabelle website, and I've found the that symmetric property in page 2 is stated as:
sym: eq x y <--> eq x y
Not sure if I am missing something here, but I assume it should be eq x y <--> eq y x.
Last updated: Dec 21 2024 at 12:33 UTC