Skip to content

Instantly share code, notes, and snippets.

View larrytheliquid's full-sized avatar

Larry Diehl larrytheliquid

View GitHub Profile
@larrytheliquid
larrytheliquid / gist:3886590
Created October 13, 2012 23:27
inductive-recursive universe for dependent types
module IRDTT where
open import Level
open import Data.Product public using ( Σ ; _,_ ; proj₁ ; proj₂ )
open import Data.Sum public using ( _⊎_ ; inj₁ ; inj₂ )
record ⊤ {a} : Set a where
constructor tt
data Type {a} : Set (suc a)
⟦_⟧ : ∀{a} → Type {a} → Set a
@larrytheliquid
larrytheliquid / init.el
Created September 4, 2012 18:12
replace super and subscripts with a font that renders in emacs 24 on osx
(set-fontset-font t '(#x2080 . #x00208e) "Monoco")
(set-fontset-font t '(#x002070 . #x00207e) "Monoco")
@larrytheliquid
larrytheliquid / narrow-slides-mode.el
Created August 28, 2012 21:38
Not actually a mode, just a quick hack for a presentation.
(defvar slide-delimiter
"----------------------------------------------------------------------"
"Delimiter used for changing slides")
(defun narrow-to-slide ()
(interactive)
(search-forward slide-delimiter)
(next-line)
(let ((start (point)))
(search-forward slide-delimiter)
@larrytheliquid
larrytheliquid / Maths.agda
Created July 15, 2011 03:10
Rudimentary but working Agda -> Ruby compilation & use examples (see test file at bottom) http://github.com/larrytheliquid/agda-rb
module Maths where
data Nat : Set where
zero : Nat
suc : Nat → Nat
plus : Nat → Nat → Nat
plus zero n = n
plus (suc m) n = suc (plus m n)
@larrytheliquid
larrytheliquid / latex_updater.rb
Created April 27, 2011 03:01
tex = ARGV[0]
modified_at = File.mtime tex
puts "Starting from: #{modified_at}"
loop do
if modified_at != (mtime = File.mtime tex)
modified_at = mtime
`pdflatex #{tex}`
puts "Recompiled for: #{modified_at}"
end
@larrytheliquid
larrytheliquid / gist:788825
Created January 20, 2011 22:31
\usepackage[mathletters]{ucs}
\usepackage[utf8]{inputenc}
@larrytheliquid
larrytheliquid / my-plt-ish-books.txt
Created October 17, 2010 04:58
programming language theory: my current batch of books related to the topic, should help to get a feel of the basics
Mathematical Logic - Kleene
Basic Category Theory for Computer Scientists - Pierce
A Book of Abstract Algebra - Pinter
Conceptual Mathematics - Lawvere & Schanuel
An Introduction to Formal Logic - Smith
To Mock A Mockingbird - Smullyan
Introduction To Logic - Tarski
Purely Functional Data Structures - Okasaki
Topoi: The Categorial Analysis of Logic - Goldblatt
Lectures on the Curry-Howard Isomorphism - Sorensen, Urzyczyn
@larrytheliquid
larrytheliquid / Decimal.agda
Created August 19, 2010 23:25
module Decimal where
open import Data.Nat
infixr 5 _∷_
infixl 8 _^_
_^_ : ℕ → ℕ → ℕ
n ^ zero = 1
n ^ (suc m) = n * (n ^ m)
@larrytheliquid
larrytheliquid / Solve.oz
Created June 25, 2010 06:45
fun comparison between solving static Twelf indexed type family relations & dynamic Oz relational computation functions
% $Id: Solve.oz,v 1.1 2007/11/26 20:13:05 leavens Exp leavens $
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Mozart System Supplements
% This file gives the extensions to the basic Mozart system that
% are used in the book "Concepts, Techniques, and Models of Computer
% Programming". The contents of this file can be put in the .ozrc
% file in your home directory, which will cause it to be loaded
% automatically when Mozart starts up.
@larrytheliquid
larrytheliquid / gist:275766
Created January 12, 2010 23:44
larrytheliquid@netbooktheliquid:~/src/testhubris$ Hubrify foo2.hs --module Bar --output foo2.bundle
Candidates: ["l"]
Language.Ruby.Hubris.wrap Bar.l (fromIntegral $ fromEnum $ Language.Ruby.Hubris.Binding.RUBY_Qtrue)
type of wrap.l is "Language.Ruby.Hubris.Binding.Value"
Exportable: ["l"]
{-# LANGUAGE ForeignFunctionInterface, ScopedTypeVariables #-}
module Language.Ruby.Hubris.Exports.Bar where
import Language.Ruby.Hubris
import qualified Prelude as P()
import Language.Ruby.Hubris.Binding