def bitw.index_none

bend-osdev-algo@0.1.0.0 · PROOF.bend:461

import Base
import bend-osdev-algo@0.1.0.0/algo.bend as A

461def bitw.index_none(m: Nat, e: {A.bitw.index(m) == None{} : Maybe<&2, Nat>}) -> {m == 0n : Nat}:
462  match m:
463    case 0n:
464      {==}
465    case 1n+i:
466      Empty.absurd({1n+i == 0n : Nat}, absurd.sn(i, e))