def word_bit

bendtorch-core@0.1.0.0 · src/storage/arith.bend:117

import Base

117def word_bit(-p: Nat, +b: Bool, -t: Word(p)) -> {bit(b, Word.to_nat(p, t)) == Word.to_nat(1n+p, WCon{b, t}) : Nat}:
118  match b:
119    case False{}:
120      {==}
121    case True{}:
122      {==}