Notation for executable float32 semantics (IEEE32Exec)

Mathlib tends to keep non-trivial notation scoped (see e.g. scoped[FinsetFamily] notation …), so downstream code can opt in with open scoped … rather than inheriting new syntax globally.

This file follows that pattern for TorchLean's executable IEEE-754 binary32 model:

open scoped IEEE754

-- constants:
∞₃₂        -- `IEEE32Exec.posInf`
-∞₃₂       -- `IEEE32Exec.negInf`
NaN₃₂      -- `IEEE32Exec.canonicalNaN`

-- decoding semantics:
⟦x⟧₃₂      -- `IEEE32Exec.toReal x`
⟦x⟧₃₂ᴱ     -- `IEEE32Exec.toEReal x`

The notation here is kept small: it targets readability in docs/proofs, not a full DSL.

Scoped constants

def IEEE754.«term∞₃₂» : Lean.ParserDescr

+∞ as an executable binary32 constant.

def IEEE754.«term-∞₃₂» : Lean.ParserDescr

-∞ as an executable binary32 constant.

def IEEE754.termNaN₃₂ : Lean.ParserDescr

A canonical quiet NaN payload used by the executable kernel.

Scoped decoding notation

def IEEE754.«term⟦_⟧₃₂» : Lean.ParserDescr

Scoped notation for decoding an executable float32 to ℝ (via IEEE32Exec.toReal).

def IEEE754.«term⟦_⟧₃₂ᴱ» : Lean.ParserDescr

Scoped notation for decoding an executable float32 to EReal (via IEEE32Exec.toEReal).