Documentation

Lean.AuxRecursor

Equations
def Lean.mkRecOnName (indDeclName : Lean.Name) :
Equations
Equations
Equations
def Lean.mkBelowName (indDeclName : Lean.Name) :
Equations
Equations
Equations
@[export lean_is_aux_recursor]
Equations
Equations
@[export lean_is_no_confusion]
Equations