def seq.step

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

import Base
import bend-kit-collections@0.1.4.1/order.bend as Order

4023# One step of eq on the heads a and b, with the tails' result as ih.
4024def seq.step(
4025  +a: U32, +b: U32, +s: String, +t: String, c: Cmp, h: {U32.cmp(a, b) == c : Cmp},
4026  e: {Order.string.fin(c, Order.string(s, t)) == EQ{} : Cmp},
4027  ih: {Order.string(s, t) == EQ{} : Cmp} -> {s == t : String}
4028) -> {SCon{Chr{a}, s} == SCon{Chr{b}, t} : String}:
4029  match c:
4030    case LT{}:
4031      ne_absurd({SCon{Chr{a}, s} == SCon{Chr{b}, t} : String}, LT{}, {==}, e)
4032    case EQ{}:
4033      +ea = ucmp_eq(a, b, h)
4034      +es = ih(e)
4035      %ea : {SCon{Chr{a}, s} == SCon{Chr{_}, t} : String}
4036      %es : {SCon{Chr{a}, s} == SCon{Chr{a}, _} : String}
4037      {==}
4038    case GT{}:
4039      ne_absurd({SCon{Chr{a}, s} == SCon{Chr{b}, t} : String}, GT{}, {==}, e)