def sfrom.base

bend-kit-collections@0.1.4.1 · PROOF.bend:166

import Base
import bend-mathlib@0.7.4.0/bool.bend as MBool
import bend-kit-collections@0.1.4.1/LAWS.bend as Laws

166def sfrom.base(
167  ~K: Data, ~cmp: K -> K -> Cmp, lb: Maybe<&2, K>, acc: List<&2, K>,
168  lt: {lt_m(~K, ~cmp, lb, head(K, acc)) == True{} : Bool},
169  sa: {Laws.sorted(~K, ~cmp, acc) == True{} : Bool}
170) -> {sfrom(~K, ~cmp, lb, acc) == True{} : Bool}:
171  match lb acc:
172    case None{} _:
173      sa
174    case Some{b} Nil{}:
175      {==}
176    case Some{+b} Con{+h, t}:
177      MBool.and_eq_true(Cmp.is_lt(cmp(b, h)), Laws.sorted.go(~K, ~cmp, t, h), lt, sa)