String.cmp.fin: def of Base
Import: import Base
Lines 2004-2013 of Base/base.bend: https://jend.leeeet.dev/read.txt?path=Base/base.bend&start_line=2004&end_line=2013

import Base

def String.cmp.fin(t1: String, t2: String, hc: (Char & Char) & Cmp) ->
  (String & String) & Cmp:
  ((h1b, h2b), c) = hc
  match c:
    case LT{}:
      ((SCon{h1b, t1}, SCon{h2b, t2}), LT{})
    case EQ{}:
      String.cmp.rec(h1b, h2b, String.cmp(t1, t2))
    case GT{}:
      ((SCon{h1b, t1}, SCon{h2b, t2}), GT{})

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Char
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.cmp.rec