def word.eq

bend-osdev-algo@0.1.0.0 · PROOF.bend:1040

import Base

1040def word.eq(n: Nat, a: Word(n), b: Word(n), e: {Cmp.is_eq(Word.cmp(n, a, b)) == True{} : Bool}) -> {a == b : Word(n)}:
1041  match n:
1042    case 0n:
1043      match a b:
1044        case WNil{} WNil{}:
1045          {==}
1046    case 1n+ +p:
1047      match a b:
1048        case WCon{+x, +at} WCon{+y, +bt}:
1049          +e2 = e
1050          %word.eq(p, at, bt, word.eq_tail(Word.cmp(p, at, bt), x, y, e2)) : {WCon{x, at} == WCon{y, _} : Word(1n+p)}
1051          %word.eq_head(Word.cmp(p, at, bt), x, y, e2) : {WCon{x, at} == WCon{_, at} : Word(1n+p)}
1052          {==}