def wn.cmp_refl

bend-osdev-word64@0.1.1.0 · proof_value.bend:249

import bend-osdev-word64@0.1.1.0/proof_value.bend as ProofValue

import Base

249def wn.cmp_refl(a: Nat) -> {Nat.cmp(a, a) == EQ{} : Cmp}:
250  match a:
251    case 0n:
252      {==}
253    case 1n+p:
254      wn.cmp_refl(p)

Uses (3)

Used by (1)

bend-osdev-word64@0.1.1.0/proof_value:wv.halves_eq