Skip to content

Instantly share code, notes, and snippets.

Avatar

Stuart Gaλe bishboria

View GitHub Profile
@bishboria
bishboria / springer-free-maths-books.md
Last active Apr 6, 2021
Springer made a bunch of books available for free, these were the direct links
@bishboria
bishboria / ConsCarCdr.js
Created Aug 25, 2011
JavaScript implementation of cons, car and cdr
View ConsCarCdr.js
function cons(x, y) {
return function(w) { return w(x, y) };
};
function car(z) {
return z(function(x, y) { return x });
};
function cdr(z) {
return z(function(x, y) { return y });
@bishboria
bishboria / multiplication.agda
Last active Oct 23, 2016
Exercise: Encode multiplication as a type in Agda
View multiplication.agda
-- This was an exercise: to encode _×_≡_ using _+_≡_
module Multiplication where
open import Data.Nat using (ℕ; suc; zero)
-- Addition encoded as a type
data _+_≡_ : Set where
zp : {n} zero + n ≡ n
sp : {m n k} m + n ≡ k suc m + n ≡ suc k
View ContextTransitivity.agda
CxTrans : forall {n m o} {De : Cx n} {De' : Cx m} {De'' : Cx o}
(p : n ≤′ m)
(q : m ≤′ o)
CxLe p De De'
CxLe q De' De''
CxLe (ℕtrans p q) De De''
@bishboria
bishboria / syntax.agda3
Last active Aug 31, 2016
I want this in Agda
View syntax.agda3
-- This isn't real Agda code, but it's
-- something i find i want to have regularly.
-- As a simple example, the Integers.
data Int : Set where
ze : Int
su : Int -> Int
- (su x) : Int -> Int
- _ ()
su (- x) ()
View sussudio.agda
data Ohoh : Set where
dio : Ohoh
su : Ohoh -> Ohoh
val : Ohoh
val = su (su (su dio))
View agdarewritebug.md

Agda rewrite bug (Update at end)

Agda version: 2.5.1.1 OSX: 10.11.5

This definitely seems to be a bug this time, when trying to use the rewrite functionality on implementing Conor and James' Levitation With A Lambda paper I have the following code (fragment):

actNVaIm {Γ} (Λ' b T) t rewrite wkAcVaIm {Γ} b = ?

View agsy.md

Levels of computation in Agsy?

Agda version: 2.5.1.1 (homebrew install) OSX: 10.11.5

When reimplementing Conor & James' paper Levitation With A Lambda, I'm noticing something interesting/a possible bug in the goal & context buffer.

Reached the point in the paper where we are implementing module LAWS and filling in the body of actNVaIm, (K' A) : Desc.

View minimal-oo.scm
; Minimal "object oriented" scaffolding
(define (object methods)
(lambda (label method-parameters)
((cdr (assoc label methods)) method-parameters)))
; declaration: easily do funkier state stuff here
(define (person name dob)
(object `( (name . ,(lambda () name))
(age . ,(lambda (today) (- today dob)))))) ; absolute nonsense, but an example of param passing
@bishboria
bishboria / git-stashes.sh
Created Feb 21, 2016
Find all git stashes
View git-stashes.sh
find . -iname .git | xargs -I % sh -c 'cd %/..; pwd; git stash list | sed "s/^/ /"'