Poly.top: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/poly.bend as Poly
Lines 34-42 of bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/poly.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/poly.bend&start_line=34&end_line=42

import Base

# The coefficient of x^(n-1) of a residue.
def top(n: Nat, w: Word(n)) -> Bool:
  match n w:
    case 0n WNil{}:
      False{}
    case 1n WCon{b, t}:
      b
    case 2n+p WCon{b, t}:
      top(1n+p, t)

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.Nil