Skip to content

Instantly share code, notes, and snippets.

View dpiponi's full-sized avatar
🧱
In material form

Dan Piponi dpiponi

🧱
In material form
View GitHub Profile
@wakita
wakita / Makefile
Last active July 21, 2023 08:53
Metal compute shader example
SDK = xcrun -sdk macosx
all: compute.metallib compute
compute.metallib: Compute.metal
# Metal intermediate representation (.air)
$(SDK) metal -c -Wall -Wextra -std=osx-metal2.0 -o /tmp/Compute.air $^
# Metal library (.metallib)
$(SDK) metallib -o $@ /tmp/Compute.air
@bishboria
bishboria / springer-free-maths-books.md
Last active April 25, 2024 06:27
Springer made a bunch of books available for free, these were the direct links
@gelisam
gelisam / Loeb.hs
Last active July 6, 2017 13:39
Encoding provability logic and Löb's theorem in Haskell.
-- | A proof of Löb's theorem in Haskell, in reply to [1].
--
-- Like Dan Piponi's post on the subject [2], we end up with a function which is
-- basically a spreadsheet evaluator.
--
-- Unlike Dan's post, our proof of Löb's theorem follows the Wikipedia
-- proof [3] very closely. Since the proof is using provability logic, we
-- need to encode the rules of provability logic inside Haskell.
-- In particular, we avoid the common mistake of representing the rule
--