WordEncoding.split: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding
Lines 158-165 of stelliferous@0.0.2.0/proofs/word_encoding.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/word_encoding.bend&start_line=158&end_line=165

import Base

def split(+n: Nat, +m: Nat, w: Word(Nat.add(n,m))) -> Split<n,m>:
  match n:
    case 0n:
      Parts{WNil{},w}
    case 1n+ +p:
      match w:
        case WCon{b,rest}:
          prepend(p,m,b,split(p,m,rest))

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  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.Nil
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_encoding.bend&name=Split
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_encoding.bend&name=prepend