Email Gateway (Aug 22 2022 at 20:44): Email Gateway (Aug 22 2022 at 20:44):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hi!
Is there a function in the Isabelle standard library that swaps the
arguments of a binary function, that is, a function flip that is
essentially defined as flip f y x ≡ f x y?
All the best,
Wolfgang
Email Gateway (Aug 22 2022 at 20:44):From: Makarius <makarius@sketis.net>
Maybe you mean the Isabelle/HOL library. Concerning Isabelle/ML there is
no such function, because almost everything is in "canonical argument
order" according to section 0.3 of the "implementation" manual. The
explanations apply to other functional languages and logics. Hopefully
more people learn about it and thus simplify their live.
Makarius
Email Gateway (Aug 22 2022 at 20:44):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
I meant some Isabelle function that flips arguments. I didn’t write
Isabelle/HOL but just Isabelle, because I thought such a function might be implemented on the level of Isabelle/Pure.
So to rephrase: Is there an Isabelle function like Haskell’s flip
defined in some sort of standard library, perhaps the Isabelle/HOL
library?
I’m defining an inductive predicate that takes a binary function as an
argument. The definition of the predicate uses this function and its
flipped version. So it’s not that a function comes with the “wrong”
argument order, but that both argument orders are needed.
All the best,
Wolfgang
Last updated: Apr 19 2024 at 20:15 UTC