unary function to (n=1)-ary

Stream: mathlib4

[Martin Dvořák]

Do we have them already?

def nary1_of_unary {α β : Type _} (f : α → β) : (Fin 1 → α) → β :=
  fun a => f (a 0)

def nary2_of_binary {α β : Type _} (f : α → α → β) : (Fin 2 → α) → β :=
  fun a => f (a 0) (a 1)

[Eric Wieser]

We have something like this in the model theory library

[Eric Wieser]

I think there are helper constructors like docs#FirstOrder.Language.Structure.mk 2

[Martin Dvořák]

If you mean this one
https://github.com/leanprover-community/mathlib4/blob/68c7277eb809a743588fe39cd21737944bf8e6c6/Mathlib/ModelTheory/Basic.lean#L115-L116
it didn't help me.

[Eric Wieser]

I mean https://leanprover-community.github.io/mathlib4_docs/Mathlib/ModelTheory/Basic.html#FirstOrder.Language.Structure.mk%E2%82%82

[Martin Dvořák]

I could almost use FirstOrder.Language.funMap₂ if I worked with different (arguably more complicated) types.

However, as I pointed out elsewhere, I don't want to tie my code to the FirstOrder.Language from model theory.