~/jendhub

def half_le

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

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

1546# half(n) <= n
1547def half_le(+n: Nat) -> {True{} == leb(half(n), n) : Bool}:
1548  %add_zero_r(n) : {True{} == leb(half(n), _) : Bool}
1549  half_go_le(n, 0n)

Uses (6)

Used by (1)