Evaluation by reduction
Instances
- Lean.Meta.instReduceEvalBinderInfo_qq
- Lean.Meta.instReduceEvalBitVec_qq
- Lean.Meta.instReduceEvalBool_qq
- Lean.Meta.instReduceEvalFVarId_qq
- Lean.Meta.instReduceEvalFinOfNeZeroNat_qq
- Lean.Meta.instReduceEvalLevelMVarId_qq
- Lean.Meta.instReduceEvalList_qq
- Lean.Meta.instReduceEvalLiteral_qq
- Lean.Meta.instReduceEvalMVarId_qq
- Lean.Meta.instReduceEvalName
- Lean.Meta.instReduceEvalNat
- Lean.Meta.instReduceEvalOption
- Lean.Meta.instReduceEvalString
- Lean.Meta.instReduceEvalUInt64_qq
- Lean.Meta.instReduceEvalUSize_qq
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Meta.instReduceEvalName = { reduceEval := Lean.Meta.evalName✝ }