def internal_all_ge

bend-mathlib@0.8.1.0 · sort.bend:96

import bend-mathlib@0.8.1.0/sort.bend as Sort

import Base

96# A recursion, not List.all with a lambda over lo, which --verdict cannot translate (PLAN F38).
97def internal_all_ge(~A: Data, ~le: A -> A -> Bool, +lo: A, xs: List<&2, A>) -> Bool:
98  match xs:
99    case Nil{}:
100      True{}
101    case h <> t:
102      Bool.and(le(lo, h), internal_all_ge(~A, ~le, lo, t))

Uses (3)

Used by (4)