def cmp.split

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

import Base
import bend-kit-collections@0.1.4.1/omap.bend as O

501# Proves a goal about O.Cmp.case by one case per comparison result.
502def cmp.split(
503  -A: Type, -B: Type, -F: A -> B, -G: B, c: Cmp, -f1: Unit -> A,
504  -f2: Unit -> A, -f3: Unit -> A,
505  hl: {c == LT{} : Cmp} -> {F(f1(Unit{})) == G : B},
506  he: {c == EQ{} : Cmp} -> {F(f2(Unit{})) == G : B},
507  hg: {c == GT{} : Cmp} -> {F(f3(Unit{})) == G : B}
508) -> {F(O.Cmp.case(A, c, f1, f2, f3)) == G : B}:
509  match c:
510    case LT{}:
511      hl({==})
512    case EQ{}:
513      he({==})
514    case GT{}:
515      hg({==})