Title | Author(s) | Year |
---|---|---|
Intuitionistic Type Theory | Per Martin-Löf | 1984 |
On the Meanings of the Logical Constants and the Justification of the Logical Laws | Per Martin-Löf | 1996 |
[[http://mat.uab.cat/~kock/crm/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
<!DOCTYPE html> | |
<html> | |
<head> | |
<script src="https://code.jquery.com/jquery-2.1.1.min.js"></script> | |
<meta charset="utf-8"> | |
<title>JS Bin</title> | |
<style id="jsbin-css"> | |
#main{ | |
padding:4px; | |
cursor: pointer; |
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
(defmacro update-in* | |
"'Updates' a value in a nested associative structure, where ks is a | |
sequence of keys and f is a function that will take the old value | |
and any supplied args and return the new value, and returns a new | |
nested structure. If any levels do not exist, hash-maps will be | |
created." | |
([m [k & ks] f & args] | |
(if ks | |
`(let [m# ~m k# ~k] (assoc m# k# (update-in* (get m# k#) ~ks ~f ~@args))) | |
`(let [m# ~m k# ~k] (assoc m# k# (~f (get m# k#) ~@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
; originally posted on https://github.com/rodricios/eatiht/issues/2#issuecomment-67769343 | |
(import | |
[collections [Counter]] | |
[cookielib [CookieJar]] | |
[lxml.etree [HTML tostring]] | |
[urllib2 [build-opener HTTPCookieProcessor]]) | |
(def *min-length* 20) | |
(def *text-xpath* (+ "//body//*[not(self::script or self::style or self::i or self::b or self::strong or self::span or self::a)]/text()[string-length(normalize-space()) > " (str *min-length*) "]/..")) |
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
# http://www.artima.com/weblogs/viewpost.jsp?thread=101605 | |
@multimethod(int, int) | |
def foo(a, b): | |
return a + b | |
@multimethod(float, float): | |
def foo(a, b): | |
return int(a+b) | |
@multimethod(str, str): | |
def foo(a, b): |
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
(ns ^{:doc "Evaluator from ch1 of lisp in small pieces. Warning: | |
NON-IDIOMATIC clojure!"} | |
lisp.chapter1.eval | |
(:refer-clojure :exclude [extend])) | |
(defn wrong [& msgs] | |
(throw (RuntimeException. (apply str msgs)))) | |
;; -- runtime support, environments are represented as a seq of pairs, | |
;; -- stored in an atom. Non-idiomatic but faithful to the book. |
This simple script will take a picture of a whiteboard and use parts of the ImageMagick library with sane defaults to clean it up tremendously.
The script is here:
#!/bin/bash
convert "$1" -morphology Convolve DoG:15,100,0 -negate -normalize -blur 0x1 -channel RBG -level 60%,91%,0.1 "$2"
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
// Works as expected... if one gets it to compile | |
#include <libzfs.h> | |
#include <stdio.h> | |
#include <stdlib.h> | |
int zp_iter(zpool_handle_t *z, void *a) { | |
printf("name:\t%s\n", zpool_get_name(z)); | |
return 0; | |
} |
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
Lazy, infinite recursive sequences in Bash (like in Haskell, if you squint). | |
I was inspired by the beautiful Haskell zipWith implementation of the Fibonacci sequence `fibs = 0 : 1 : zipWith (+) fibs (tail fibs)` | |
to find an equivalent in bash using 'coroutines' and recursive pipes. | |
My original experiments were https://twitter.com/tavisrudd/status/367164339716751360 | |
"fun w/ recursive pipes: e=echo;mkfifo fib;{ $e 0 1 1 >fib &};{ while read i j k; do $e $i >&2; $e $j $k $(($j+$k));sleep .4; done;}<fib>fib" | |
and https://twitter.com/tavisrudd/status/367142071489937408 | |
"o=ouro;b=boros;mkfifo $o$b;e=echo; { $e $o > $o$b & }; { while read s;do $e $s>&2;case $s in $o)$e $b;;*)$e $o; esac; done; }<$o$b >$o$b" |
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
From welch@thor.oar.net Thu Oct 20 16:53:41 EDT 1994 | |
Article: 15160 of comp.lang.lisp | |
Path: cantaloupe.srv.cs.cmu.edu!das-news2.harvard.edu!news2.near.net!news.mathworks.com!usenet.eel.ufl.edu!usenet.cis.ufl.edu!caen!math.ohio-state.edu!magnus.acs.ohio-state.edu!usenet.ins.cwru.edu!ns.mcs.kent.edu!kira.cc.uakron.edu!malgudi.oar.net!malgudi.oar.net!welch | |
From: welch@thor.oar.net (Arun Welch) | |
Newsgroups: comp.lang.lisp | |
Subject: CL History (was Re: Why do people like C?) | |
Date: 20 Oct 94 15:34:10 | |
Organization: OARnet | |
Lines: 3244 | |
Message-ID: <WELCH.94Oct20153410@thor.oar.net> |