def internal_cmp_refl
bend-mathlib@0.8.1.0 · string.bend:167
import bend-mathlib@0.8.1.0/string.bend as String
import Base
167def internal_cmp_refl(s: String) -> {((s, s), EQ{}) == String.cmp(s, s) : (String & String) & Cmp}:
168 match s:
169 case SNil{}:
170 {==}
171 case SCon{h, t}:
172 match h:
173 case Chr{x}:
174 %internal_u32_cmp_refl(x) : {((SCon{Chr{x}, t}, SCon{Chr{x}, t}), EQ{}) == String.cmp.fin(t, t, ((Chr{x}, Chr{x}), _)) : (String & String) & Cmp}
175 %internal_cmp_refl(t) : {((SCon{Chr{x}, t}, SCon{Chr{x}, t}), EQ{}) == String.cmp.rec(Chr{x}, Chr{x}, _) : (String & String) & Cmp}
176 {==}