Conv

📁 Source: Mathlib/Tactic/Conv.lean

Statistics

Metric	Count
Definitions convLHS, convRHS, convRefine_, convRun_conv_, dischargeConv, elabDischargeConv, withReducible, «command#conv_=>_», «command#simpOnly_=>__», «command#whnfR_», «command#whnf_», «convConvIn__=>_»	12
Theorems	0
Total	12

Mathlib.Tactic.Conv

Definitions

Name	Category	Theorems
convLHS 📖	CompOp	—
convRHS 📖	CompOp	—
convRefine_ 📖	CompOp	—
convRun_conv_ 📖	CompOp	—
dischargeConv 📖	CompOp	—
elabDischargeConv 📖	CompOp	—
withReducible 📖	CompOp	—
«command#conv_=>_» 📖	CompOp	—
«command#simpOnly_=>__» 📖	CompOp	—
«command#whnfR_» 📖	CompOp	—
«command#whnf_» 📖	CompOp	—
«convConvIn__=>_» 📖	CompOp	—

---

← Back to Index