def ord.nums

ezx@1.11.0.0 · src/git/git.bend:407

import Base

407def ord.nums(left: List<&2, Nat>, right: List<&2, Nat>) -> Ord:
408  match left right:
409    case Nil{} Nil{}:
410      Eq{}
411    case Nil{} Con{+h, t}:
412      ord.pad(h <> t)
413    case Con{+h, t} Nil{}:
414      ord.flip(ord.pad(h <> t))
415    case Con{+ha, ta} Con{+hb, tb}:
416      ord.nums.at(ord.nat(Nat.is_eq(ha, hb), Nat.is_lt(ha, hb)),
417        _u => ord.nums(ta, tb))