{{ message }}

Instantly share code, notes, and snippets.

# Stuart Gaλe bishboria

Last active Apr 6, 2021
Springer made a bunch of books available for free, these were the direct links
View springer-free-maths-books.md
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 });
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
Created Sep 23, 2016
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''
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) ()
Created Aug 20, 2016
View sussudio.agda
 data Ohoh : Set where dio : Ohoh su : Ohoh -> Ohoh val : Ohoh val = su (su (su dio))
Last active Jul 4, 2016
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 = ?`

Created Jul 4, 2016
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`.

Last active Apr 2, 2016
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
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/^/ /"'