AlphaGitHub
Source/Packages

Std.Numeric.Profile

packages/foundation/standard/src/Std/Numeric/Profile.alpha

736 lines139 declarations26.5 KiBSHA-256 2450517e3794
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 258–267

stdApproximationIsExact

Full file
258def stdApproximationIsExact =
259  (lambda unrestricted bound : (family StdApproximation) .
260    (eliminate
261      StdApproximation
262      (lambda unrestricted current : (family StdApproximation) . Nat)
263      bound
264      (branch StdApproximationExact . (succ zero))
265      (branch StdApproximationMaxUlp ulp . zero)
266      (branch StdApproximationUnmeasured . zero)
267      (branch StdApproximationUnsupported . zero)))

The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.