Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] power class instantiation

Email Gateway (Aug 18 2022 at 15:28):

From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello

I need to instantiate the class power to sets, something like:

instantiation "set" :: (power) power
begin

definition "one = {1}"
definition "A * B = {x . ? a in A . ? b in B . x = a * b}
...
However I get an error in the first line of this declaration.

*** Logical type constructor expected: "set"
*** At command "instantiation".

Best regards,

Viorel Preoteasa

Email Gateway (Aug 18 2022 at 15:29):

From: Tobias Nipkow <nipkow@in.tum.de>
Unfortunately "set" is not a type constructor but an abbreviation for
"'a => bool". Hence you cannot instatiate any class with "set". For an
alternative search for ^^ in Nat.thy or Transitive_Closure.thy.

Tobias

Viorel Preoteasa schrieb:

Last updated: Apr 24 2024 at 04:17 UTC