Proof-indexed views of numerical systems

Every NumericalSystem has one runtime carrier, S.Code. The abbreviations in this module attach an erased proof of what a stored code denotes; they do not introduce another representation.

S.At value tracks the complete NumericalValue, including infinity and exceptional encodings. S.AtFinite x is the ordinary finite specialization.

@[reducible, inline]

abbrev FloatLib.Numerics.NumericalSystem.At (S : NumericalSystem) (value : NumericalValue S.Scalar) : Type u_1

A runtime code bundled with an erased proof of its complete denotation.

@[reducible, inline]

abbrev FloatLib.Numerics.NumericalSystem.AtFinite (S : NumericalSystem) (value : S.Scalar) : Type u_1

A runtime code bundled with an erased proof of its ordinary finite value.

@[inline]

def FloatLib.Numerics.NumericalSystem.At.ofCode (S : NumericalSystem) (code : S.Code) : S.At (S.denote code)

Attach the denotation computed by a numerical system to an existing runtime code.

@[simp]

theorem FloatLib.Numerics.NumericalSystem.At.denote {S : NumericalSystem} {value : NumericalValue S.Scalar} (code : S.At value) : S.denote code.val = value

The bundled runtime code has its indexed complete denotation.

@[inline]

def FloatLib.Numerics.NumericalSystem.AtFinite.ofRepresents {S : NumericalSystem} {value : S.Scalar} (code : S.Code) (hcode : S.Represents code value) : S.AtFinite value

Attach an existing finite representation proof to its runtime code.

@[simp]

theorem FloatLib.Numerics.NumericalSystem.AtFinite.represents {S : NumericalSystem} {value : S.Scalar} (code : S.AtFinite value) : S.Represents code.val value

The bundled runtime code represents its indexed finite value.