type Numeric.Fits

gralha-bendquest@0.1.0.0 · numeric.bend:222

import gralha-bendquest@0.1.0.0/numeric.bend as Numeric

import Base

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

Uses (3)

Used by (6)