Fp16 Dtype#92

Merged

seanmcl merged 7 commits into

leanprover:mainfrom

SmoothThunk:Float16

Jun 30, 2026

Commits on Jun 25, 2026

PR revision: fix fp16 conversion bugs, add tests, added PBT for addition case, thread fp16 through all functions that need it, replaced occurence of unicode <- to <- for consistency
SmoothThunk
committed

Commits on Jun 29, 2026

Fix shift wrap in subnormal encoder, NaN decoder preserves NaN sign bit, -0.0 PBT, remove unused code in join, and other unused functions.
SmoothThunk
committed

Commits on Jun 30, 2026

Rewrite join using recursion and fix self-cast PBT range guard
SmoothThunk
committed