def zero_small

bendtorch-core@0.1.0.0 · src/shape/construct_proofs.bend:34

import bendtorch-core@0.1.0.0/src/shape/construct_proofs.bend as ConstructProofs
import Base

34def zero_small(+size: Nat) -> {True{} == Bool.or(Nat.is_eq(size, 0n), Nat.is_le(0n, 1048576n)) : Bool}:
35  match size:
36    case 0n:
37      {==}
38    case 1n+q:
39      {==}

Uses (5)

Used by (1)