def wd.eq

bend-osdev-u32@0.1.0.0 · PROOF_order.bend:191

import Base

191def wd.eq(n: Nat, a: Word(n), b: Word(n), +e: {Word.cmp(n, a, b) == EQ{} : Cmp}) -> {a == b : Word(n)}:
192  match n:
193    case 0n:
194      match a b:
195        case WNil{} WNil{}:
196          {==}
197    case 1n+ +p:
198      match a b:
199        case WCon{+x, +at} WCon{+y, +bt}:
200          %wd.eq(p, at, bt, wd.fin_eq_tail(Word.cmp(p, at, bt), x, y, e)) : {WCon{x, at} == WCon{y, _} : Word(1n+p)}
201          %wd.fin_eq_head(Word.cmp(p, at, bt), x, y, e) : {WCon{x, at} == WCon{_, at} : Word(1n+p)}
202          {==}