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
# gcc -Wall -o match match.c && ./match | |
# | |
#include <stdio.h> | |
#include <string.h> | |
#include <regex.h> | |
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
* Les: Getting more comfortable with HoTT - Talk: "Bluffers Guide to HoTT" | |
History - Barber's Paradoxes, etc. | |
Russell stratifying set theory | |
Martin Löf in the 1970s | |
In TT - Say term x is of type t -> `x : t` | |
This is a judgement | |
Curry Howard - Types and terms = Conjecture/proposition and Proof | |
Things become interesting in the presence of equality | |
equality is always with respect to some type | |
exists t -> x:t = y:t |
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
#include <geanyplugin.h> | |
GeanyData *geany_data; | |
GeanyPlugin *geany_plugin; | |
GeanyFunctions *geany_functions; | |
PLUGIN_VERSION_CHECK(211); | |
PLUGIN_SET_INFO("Tab Sort", | |
"Automatically keeps document tabs sorted", |
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 Control.Applicative ((<$>)) | |
center :: String -> Int -> String | |
center s n = spaces ++ s ++ spaces | |
where spaces = replicate ((n - length s) `div` 2) ' ' | |
-- http://www.haskell.org/haskellwiki/Blow_your_mind, Ctrl-F "pascal" | |
pascal :: [[Int]] | |
pascal = iterate (\row -> zipWith (+) ([0] ++ row) (row ++ [0])) [1] |