~/jendhub

def h.wcmp_refl

bend-kit-collections@0.1.4.1 · PROOF.bend:1753

import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF
import Base
import bend-mathlib@0.7.4.0/bool.bend as MBool

1753# U32 equality is Word equality, so is_eq is reflexive and sound.
1754def h.wcmp_refl(n: Nat, w: Word(n)) -> {Word.cmp(n, w, w) == EQ{} : Cmp}:
1755  match n:
1756    case 0n:
1757      {==}
1758    case 1n+p:
1759      match w:
1760        case WCon{+b, +t}:
1761          %Equal.sym(Cmp, Word.cmp(p, t, t), EQ{}, h.wcmp_refl(p, t)) : {Word.cmp.fin(b, b, _) == EQ{} : Cmp}
1762          MBool.cmp_refl(b)

Uses (8)

Used by (3)