~/jendhub

def pow2_pos

bend-ml-tensor-array@0.1.19.0 · main.bend:673

import bend-ml-tensor-array@0.1.19.0/main.bend as BendMlTensorArray
import Base

673# 1 <= 2^d
674def pow2_pos(d: Nat) -> {True{} == leb(1n, pow2(d)) : Bool}:
675  match d:
676    case 0n:
677      {==}
678    case 1n++q:
679      leb_up(1n, pow2(q), pow2(q), pow2_pos(q))

Uses (5)

Used by (1)