def wdiff

lawful-words@0.1.0.0 · proof_word.bend:918

import Base

918# The lowest bit where two words differ (0 if they are equal).
919def wdiff(n: Nat, a: Word(n), b: Word(n)) -> Nat:
920  match n:
921    case 0n:
922      0n
923    case 1n+p:
924      match a b:
925        case WCon{False{}, at} WCon{False{}, bt}:
926          1n+wdiff(p, at, bt)
927        case WCon{False{}, at} WCon{True{}, bt}:
928          0n
929        case WCon{True{}, at} WCon{False{}, bt}:
930          0n
931        case WCon{True{}, at} WCon{True{}, bt}:
932          1n+wdiff(p, at, bt)