duplicates = multiple editions
A Classical Introduction to Modern Number Theory, Kenneth Ireland Michael Rosen
A Classical Introduction to Modern Number Theory, Kenneth Ireland Michael Rosen
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 |
-- | 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 | |
-- |