~/jendhub

def native_allocatable

stelliferous@0.0.2.0 · proofs/word_power_of_two.bend:317

import stelliferous@0.0.2.0/proofs/word_power_of_two.bend as WordPowerOfTwo
import Base

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

Uses (10)

Used by (1)