@[inline]
def
Char.reduceUnary
{α : Type u_1}
[Lean.ToExpr α]
(declName : Lean.Name)
(op : Char → α)
(arity : Nat := 1)
(e : Lean.Expr)
:
Equations
Instances For
Returns .done
for Char values.
These values should not be unfolded in the symbolic evaluator.
In regular simp
, the nested raw literal should be prevented from being converted into an
OfNat.ofNat
application.