~/jendhub

def internal_char_cmp_refl

bend-mathlib@0.8.1.0 · string.bend:153

import bend-mathlib@0.8.1.0/string.bend as String
import Base

153def internal_char_cmp_refl(c: Char) -> {((c, c), EQ{}) == Char.cmp(c, c) : (Char & Char) & Cmp}:
154  match c:
155    case Chr{x}:
156      %internal_u32_cmp_refl(x) : {((Chr{x}, Chr{x}), EQ{}) == ((Chr{x}, Chr{x}), _) : (Char & Char) & Cmp}
157      {==}

Uses (6)

Used by (1)