~/jendhub

def cmp_refl_eq

bend-collections-laws-math@1.0.0.0 · proofs/lib/u32.bend:294

import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U32
import Base

294def cmp_refl_eq(+n: Nat, +w: Word(n)) -> {Cmp.is_eq(Word.cmp(n, w, w)) == True{} : Bool}:
295  match n w:
296    case 0n WNil{}:
297      {==}
298    case 1n+p WCon{b, t}:
299      fin_refl(Word.cmp(p, t, t), b, cmp_refl_eq(p, t))

Uses (8)

Used by (1)