def not_empty

mlbend-metrics@0.1.0.0 · main.bend:192

import mlbend-metrics@0.1.0.0/main.bend as MlbendMetrics

import Base

192# the number of pairs, or why there is no answer
193def not_empty(r: Result<&1, &1, Bad, Nat>) -> Result<&1, &1, Bad, Nat>:
194  match r:
195    case Done{+n}:
196      not_empty_of(Nat.is_eq(n, 0n), n)
197    case Fail{Mismatch{expected, got}}:
198      Fail{Mismatch{expected, got}}
199    case Fail{Empty{}}:
200      Fail{Empty{}}

Uses (5)

Used by (1)

mlbend-metrics@0.1.0.0/main:pairs