Evaluation of Char.toNat, Char.val, and Char.ofNat when the argument is equal to a literal.

def Lean.Meta.Grind.propagateCharToNatUp : Propagator

Propagates x.toNat = n when x is equal to a character literal c with code point n. The proof is congrArg Char.toNat (x = c) followed by Eq.refl n, whose type n = n is accepted for c.toNat = n by the kernel, which evaluates c.toNat.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.propagateCharValUp : Propagator

Propagates x.val = n when x is equal to a character literal with code point n. See propagateCharToNatUp.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.propagateCharOfNatUp : Propagator

Propagates Char.ofNat n = c when n is equal to a numeral and c is the corresponding character literal. See propagateCharToNatUp.

Equations

• One or more equations did not get rendered due to their size.