def word_cmp_eq

lawful-words@0.1.0.0 · proof_word.bend:282

import Base

282def word_cmp_eq(+n: Nat, +a: Word(n), +b: Word(n), +e: {Word.cmp(n, a, b) == EQ{} : Cmp}) -> {a == b : Word(n)}:
283  match n:
284    case 0n:
285      match a b:
286        case WNil{} WNil{}:
287          {==}
288    case 1n+p:
289      match a b:
290        case WCon{+ab, +at} WCon{+bb, +bt}:
291          %bool_cmp_eq(ab, bb, word_fin_b(ab, bb, Word.cmp(p, at, bt), e)) : {WCon{ab, at} == WCon{_, bt} : Word(1n+p)}
292          %word_cmp_eq(p, at, bt, word_fin_t(ab, bb, Word.cmp(p, at, bt), e)) : {WCon{ab, at} == WCon{ab, _} : Word(1n+p)}
293          {==}