Word.cmp: def of Base Import: import Base Lines 1329-1336 of Base/base.bend: https://jend.leeeet.dev/read.txt?path=Base/base.bend&start_line=1329&end_line=1336 import Base def Word.cmp(n: Nat, a: Word(n), b: Word(n)) -> Cmp: match n: case 0n: EQ{} case 1n+p: match a b: case WCon{ab, at} WCon{bb, bt}: Word.cmp.fin(ab, bb, Word.cmp(p, at, bt)) Uses (5): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.cmp.fin