Structures · Logic and sets

Function.HasUncurry

Records a way to turn an element of α into a function from β to γ. The most generic use is to recursively uncurry. For instance f : α → β → γ → δ will be turned into ↿f : α × β × γ → δ. One can also add instances for bundled maps.

Defined in

Mathlib.Logic.Function.Basic

Shape

3 explicit arguments · adds uncurry