WordPowerOfTwo.native_allocatable: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/word_power_of_two.bend as WordPowerOfTwo
Lines 317-320 of stelliferous@0.0.2.0/proofs/word_power_of_two.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/word_power_of_two.bend&start_line=317&end_line=320

import Base

def native_allocatable(+depth: Nat,bound: {Nat.is_le(depth,30n) == True{} : Bool}) ->
  {U32.is_le(U32.shln(1,depth),1073741824) == True{} : Bool}:
  %Equal.sym(U32,U32.shln(1,depth),U32{power(32n,depth)},native_power(depth)) : {U32.is_le(_,1073741824) == True{} : Bool}
  power_monotone(32n,depth,30n,{==},bound)

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shln
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_power_of_two.bend&name=native_power
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_power_of_two.bend&name=power
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_power_of_two.bend&name=power_monotone