def native_nonempty_depth

stelliferous@0.0.2.0 · proofs/word_power_of_two.bend:339

import Base

339def native_nonempty_depth(+depth: Nat,positive: {Nat.is_lt(0n,U32.to_nat(U32.shln(1,depth))) == True{} : Bool}) ->
340  {Nat.is_lt(depth,32n) == True{} : Bool}:
341  nonempty_power_depth(32n,depth,
342    %native_power(depth) : {Nat.is_lt(0n,U32.to_nat(_)) == True{} : Bool} positive)