This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
# Installs agda into a folder in your home directory with sensible organization | |
# First, make an agda folder in the home dir | |
mkdir $HOME/agda | |
# Next, clone the repo | |
cd $HOME/agda | |
git clone https://github.com/agda/agda.git repo | |
cd repo |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Ltac eq_ids := | |
repeat progress match goal with | |
[i1 : id, i2 : id |- _] => extend (eq_id_dec i1 i2) | |
end. | |
Lemma subst_aexp_equiv : forall i a1 a2 st, | |
aeval st (subst_aexp i a2 a1) = aeval (update st i (aeval st a2)) a1. | |
Proof. induction a1; simpl; auto; unfold update; eq_ids; crush. Qed. | |
Hint Rewrite aeval_weakening subst_aexp_equiv. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Theorem contr_pos_eq_classic : | |
(forall P Q, (~ Q -> ~ P) -> P -> Q) -> | |
forall P, ~~ P -> P. | |
Proof. intros H P nnP. apply H with (Q := P) in nnP; intuition. Qed. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
has_type(G,abs(V,E),arr(T1,T2)) :- has_type([[V,T1]|G],E,T2). | |
has_type(G,let(I,V,E),T2) :- has_type(G,V,T1), has_type([[I,T1]|G],E,T2). | |
has_type(G,app(E1,E2),T2) :- has_type(G,E1,arr(T1,T2)), has_type(G,E2,T1). | |
has_type(G,if(C,V1,V2),T) :- has_type(C,bool), has_type(G,V1,T), has_type(G,V2,T). | |
has_type(G,I,T) :- atom(I), append(_,[[I,T]|_],G). | |
has_type([],X,bool) :- X = true ; X = false. | |
has_type(Tm,Ty) :- has_type([],Tm,Ty). | |
subst(I,V,I,V). | |
subst(I,V,app(T1,T2),app(T12,T22)) :- subst(I,V,T1,T12), subst(I,V,T2,T22). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Lob where | |
open import Data.Product | |
open import Function | |
_←→_ : Set → Set → Set | |
A ←→ B = (A → B) × (B → A) | |
postulate -- provability axioms | |
□ : Set → Set |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
--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] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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] |