Functions

📁 Source: Plausible/Functions.lean

Statistics

Metric	Count
Definitions TotalFunction, toFinmap', sampleableExt, sampleableExt, sampleableExt, apply, comp, inhabited, instRepr, repr, reprAux, shrink, dedup, insertKey	14
Theorems	0
Total	14

Plausible

Definitions

Name	Category	Theorems
TotalFunction 📖	CompData	—

Plausible.TotalFunction

Definitions

Name	Category	Theorems
apply 📖	CompOp	—
comp 📖	CompOp	—
inhabited 📖	CompOp	—
instRepr 📖	CompOp	—
repr 📖	CompOp	—
reprAux 📖	CompOp	—
shrink 📖	CompOp	—

Plausible.TotalFunction.List

Definitions

Name	Category	Theorems
toFinmap' 📖	CompOp	—

Plausible.TotalFunction.Pi

Definitions

Name	Category	Theorems
sampleableExt 📖	CompOp	—

Plausible.TotalFunction.PiPred

Definitions

Name	Category	Theorems
sampleableExt 📖	CompOp	—

Plausible.TotalFunction.PiUncurry

Definitions

Name	Category	Theorems
sampleableExt 📖	CompOp	—

Plausible.TotalFunction.shrink

Definitions

Name	Category	Theorems
dedup 📖	CompOp	—

Plausible.TotalFunction.shrink.dedup

Definitions

Name	Category	Theorems
insertKey 📖	CompOp	—

---

← Back to Index