~/jendhub

law Numeric.representable_roundtrip

gralha-bendquest@0.1.0.0 · numeric.bend:248

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

248law Numeric.representable_roundtrip:
249  for +n: Nat
250  for +k: Nat
251  for +fits: Numeric.Fits<n, k>
252  {Word.to_nat(n, Numeric.encode(n, k)) == k : Nat}

Uses (6)

Used by (1)