OfArity

📁 Source: Mathlib/Logic/Function/OfArity.lean

Statistics

Metric	Count
Definitions fromTypes_fin_const_equiv, OfArity, const, inhabited	4
Theorems fromTypes_fin_const, const_succ, const_succ_apply, const_zero, ofArity_succ, ofArity_zero	6
Total	10

Function

Definitions

Name	Category	Theorems
OfArity 📖	CompOp	5 math math: FromTypes.fromTypes_fin_const, OfArity.curryEquiv_symm_apply, ofArity_succ, ofArity_zero, OfArity.curryEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofArity_succ 📖	mathematical	—	OfArity	—	fromTypes_succ
ofArity_zero 📖	mathematical	—	OfArity	—	fromTypes_zero

Function.FromTypes

Definitions

Name	Category	Theorems
fromTypes_fin_const_equiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fromTypes_fin_const 📖	mathematical	—	Function.FromTypes Function.OfArity	—	—

Function.OfArity

Definitions

Name	Category	Theorems
const 📖	CompOp	3 math math: const_succ, const_succ_apply, const_zero
inhabited 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
const_succ 📖	mathematical	—	const	—	Function.FromTypes.const_succ
const_succ_apply 📖	mathematical	—	const	—	Function.FromTypes.const_succ_apply
const_zero 📖	mathematical	—	const	—	Function.FromTypes.const_zero

---

← Back to Index