Theorems · Definition

Function.HasUncurry.uncurry

{α : Type u_5} → {β : outParam (Type u_6)} → {γ : outParam (Type u_7)} → [self : Function.HasUncurry α β γ] → α → β → γ

Uncurrying operator. 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

Cited by

57 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

Function.HasUncurry