~/jendhub

def internal_eq_true_cmp

bend-mathlib@0.8.1.0 · string.bend:240

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

240def internal_eq_true_cmp(+a: String, +b: String, h: {String.eq(a, b) == True{} : Bool}) -> {Cmp.is_eq(Pair.snd(String & String, Cmp, String.cmp(a, b))) == True{} : Bool}:
241  %Equal.sym(Cmp, Pair.snd(String & String, Cmp, String.cmp(a, b)), String.order(a, b), internal_order_cmp(a, b)) : {Cmp.is_eq(_) == True{} : Bool}
242  h

Uses (11)

Used by (1)