Theorems · Definition

Function.eval

{α : Sort u_1} → {β : α → Sort u_4} → (x : α) → ((x : α) → β x) → β x

Evaluate a function at an argument. Useful if you want to talk about the partially applied Function.eval x : (∀ x, β x) → β x.

Defined in

Mathlib.Logic.Function.Basic

Cited by

140 results in Mathlib

Foundations

Depth 0 from the axioms, rests on 1 definitions · uses no axioms