def internal_word_eq

bend-mathlib@0.8.1.0 · string.bend:277

import Base

277def internal_word_eq(n: Nat, a: Word(n), b: Word(n), +h: {Cmp.is_eq(Word.cmp(n, a, b)) == True{} : Bool}) -> {a == b : Word(n)}:
278  match n:
279    case 0n:
280      match a b:
281        case WNil{} WNil{}:
282          {==}
283    case 1n+ +p:
284      match a b:
285        case WCon{+ab, +at} WCon{+bb, +bt}:
286          %internal_fin_head(ab, bb, Word.cmp(p, at, bt), h) : {WCon{ab, at} == WCon{_, bt} : Word(1n+p)}
287          %internal_word_eq(p, at, bt, internal_fin_tail(ab, bb, Word.cmp(p, at, bt), h)) : {WCon{ab, at} == WCon{ab, _} : Word(1n+p)}
288          {==}