def wd.fin_refl

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

import bend-osdev-u32@0.1.0.0/PROOF_order.bend as PROOFOrder

import Base

145def wd.fin_refl(x: Bool) -> {Word.cmp.fin(x, x, EQ{}) == EQ{} : Cmp}:
146  match x:
147    case True{}:
148      {==}
149    case False{}:
150      {==}

Uses (3)

Used by (1)

bend-osdev-u32@0.1.0.0/PROOF_order:wd.refl