Email Gateway (Aug 18 2022 at 14:56): Email Gateway (Aug 18 2022 at 14:56):From: Hojjat Hossein <hossein.hojjat@epfl.ch>
Hello everyone,
According to Section 6.3.1 of the tutorial the iterated composition of a relation is available with the exponentiation sign. I am not sure why I get errors in the following theory:
theory relation_exponent
imports Main
begin
value "({(1::nat,2::nat),(2::nat,3::nat)} O {(1::nat,2::nat),(2::nat,3::nat)})"
value "({(1::nat,2::nat),(2::nat,3::nat)} ^ (2::nat))"
end
The first value is fine but for the second one I get the following error:
*** Type unification failed: No type arity fun :: power
*** Type error in application: Incompatible operand type
*** Operator: op ^ :: (nat × nat => bool) => nat => nat × nat => bool
*** Operand: {(1, 2), (2, 3)} :: nat × nat => bool
*** At command "value".
I am using Isabelle2009-1.
Hossein Hojjat
EPFL
Email Gateway (Aug 18 2022 at 14:56):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
If I remember correctly, ^ was changed to ^^ for relations. Also note
that in contrast to previous Isabelle versions, relation composition (O)
now is defined such that "R O S" means: first a step in R and _then_ a
step in S.
cheers
chris
Last updated: Apr 20 2024 at 12:26 UTC