GallagherCommaJack

module Lob where

open import Data.Product
open import Function

_←→_ : Set → Set → Set
A ←→ B = (A → B) × (B → A)

postulate -- provability axioms
  □ : Set → Set

GallagherCommaJack

#!/bin/zsh
# This is a script to take literate haskell code with markdown syntax throughout and turn it into pure HTML
# Just put it in your path and run blcm
hscolour -html -lit $1 > "$2" # colorizes the document, -html specifies the format, -lit says this is literate code
if [ "$3" = "-s" ] # Same as the -s argument to pandoc
then
    pandoc -f markdown -t html "$2" > "$2.html" -Ss # Pandoc is a wonderful thing
else
    pandoc -f markdown -t html "$2" > "$2.html" -S
fi

GallagherCommaJack

This is a hybrid markdown and Literate Haskell document.  It's a blog post that I converted to pure html and posted <a href="http://blog.gallabytes.com/2014/03/isomorphism-equality-pq-and-other-ways.html">here</a>

So we'll first take as an axiom that math is based on axioms.  So far so good?
Well, an important thing to note with this is that it's really easy for axioms to have different significance - it all comes down to what metaphor you use in your brain to describe the axiomset

For example, <a href="http://blog.gallabytes.com/2014/03/miu-haskellized.html">MIU</a> seems wholly abstract, but it turned out to be isomorphic to some operations on the integers modulo 3.  And that isomorphism allowed some things to be made clear about it that weren't otherwise.

In Chapter 2, Hofstadter defines some axioms that he calls the "PQ system".  These axioms are:
<ol>
<li> The only valid characters are -, P, and Q</li>

GallagherCommaJack

--Helper and Main
isPalindrome :: Eq a => [a] -> Bool
isPalindrome xs = reverse xs == xs

main = print num4 >> print num4'

--Naive Solution (still finishes in .122 seconds with -O2)
threeDigNums :: [Int]
threeDigNums = [1000,999..100]

GallagherCommaJack

import System.Cmd (system)
import System.Environment (getArgs)
import System.FilePath (takeExtension)
import Control.Exception (IOException, bracket, handle)
import System.IO (IOMode(..), hClose, hFileSize, openFile)
import GHC.IO.Exception (ExitCode(..))

gccCom :: String -> [String] -> IO ExitCode
gccCom filepath args = system $ "gcc " ++ filepath ++ unwords args

GallagherCommaJack

data MIU = M | I | U deriving (Show, Read, Eq)
type STR = [MIU]

rep2 = concat . (replicate 2)

start = [M,I]

r1 :: STR -> STR
r1 ms = ms ++ [U]

GallagherCommaJack

au FileType haskell nmap <F5> :!runhaskell %<cr>
au FileType haskell nmap <F6> :!ghci %<cr>
au FileType haskell nmap <F7> :!ghc --make %<cr>