Skip to content

Fp16 Dtype #92

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
seanmcl merged 7 commits into from
Jun 30, 2026
Merged

Fp16 Dtype #92

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
77d8d09
Add fp32-fp16 and fp16-fp32 bit conversion functions
SmoothThunk Jun 23, 2026
88f9f40
Add fp16 case to all the Dtype pattern matches
SmoothThunk Jun 23, 2026
2012ed5
Map fp16 to f2 in npy header parsing
SmoothThunk Jun 23, 2026
95127c6
Add fp16 test case
SmoothThunk Jun 23, 2026
8d18082
PR revision: fix fp16 conversion bugs, add tests, added PBT for addit…
SmoothThunk Jun 25, 2026
073789b
Fix shift wrap in subnormal encoder, NaN decoder preserves NaN sign b…
SmoothThunk Jun 29, 2026
a118563
Rewrite join using recursion and fix self-cast PBT range guard
SmoothThunk Jun 30, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion TensorLib/ByteArray.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -241,7 +241,7 @@ private local instance : Shrinkable ByteArray where

private local instance : SampleableExt ByteArray :=
SampleableExt.mkSelfContained do
let data ← SampleableExt.interpSample (Array UInt8)
let data <- SampleableExt.interpSample (Array UInt8)
return ByteArray.mk data

/--
Expand Down
2 changes: 1 addition & 1 deletion TensorLib/Common.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@ example (x y : Nat) :

local instance : SampleableExt (Nat × Nat) :=
SampleableExt.mkSelfContained do
let x ← SampleableExt.interpSample Nat
let x <- SampleableExt.interpSample Nat
let n <- SampleableExt.interpSample Nat
return (x * n, x)

Expand Down
Loading
Loading