Re: [isabelle] Equivalent of Haskell’s `flip` function



Am Sonntag, den 13.10.2019, 20:27 +0200 schrieb Makarius:
> On 13/10/2019 20:12, Wolfgang Jeltsch wrote:
> 
> 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`?
> 
> 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.

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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.