~/jendhub

def pos_p

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

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

681# 1 <= p when p = 2^d
682def pos_p(d: Nat, p: Nat, i1: {p == pow2(d) : Nat}) -> {True{} == leb(1n, p) : Bool}:
683  %Equal.sym(Nat, p, pow2(d), i1) : {True{} == leb(1n, _) : Bool}
684  pow2_pos(d)

Uses (6)

Used by (1)