Numeric.Numeric.Fits: type of gralha-bendquest@0.1.0.0
Import: import gralha-bendquest@0.1.0.0/numeric.bend as Numeric
Lines 222-226 of gralha-bendquest@0.1.0.0/numeric.bend: https://jend.leeeet.dev/read.txt?path=gralha-bendquest@0.1.0.0/numeric.bend&start_line=222&end_line=226

import Base

# A representability witness avoids evaluating a closed 2^32-sized unary
# bound during type conversion. It carries an actual word with the exact
# natural value; it is not an assumed upper bound.
type Numeric.Fits<-n: Nat, -k: Nat> is Data:
  Numeric.Fits{word: Word(n), exact: {Word.to_nat(n, word) == k : Nat}}

Uses (3):
  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.to_nat