Skip to content

Instantly share code, notes, and snippets.


Stuart Gaλe bishboria

View GitHub Profile
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 / 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))

Agda rewrite bug (Update at end)

Agda version: 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 = ?


Levels of computation in Agsy?

Agda version: (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 /
Created Feb 21, 2016
Find all git stashes
find . -iname .git | xargs -I % sh -c 'cd %/..; pwd; git stash list | sed "s/^/ /"'
bishboria /
Last active Oct 16, 2020
Springer made a bunch of books available for free, these were the direct links
bishboria /
Last active Aug 31, 2015
Animated stuff when growing up

I want to have a list of the cartoons/films that I watched as a child. I have flashbacks of themetunes and images, but can't always work out what they are.

Updates will add more shows, and screenshots/youtube links if possible

  • Trapdoor
  • Transformers
  • Starcom
  • Centurions
  • Mask
  • Adventures of Teddy Ruxpin
bishboria / make output
Last active Dec 28, 2015
opengenera not working
View make output
if test -z "$(which vagrant)" ; then \
echo "### need to install vagrant"; \
echo "try: sudo gem install vagrant"; \
if test -z "$(vagrant box list | grep -w opengenera)" ; then \
make; \
vagrant box add opengenera; \
if test -z "$(which veewee)" ; then \
echo "### need to install veewee"; \
You can’t perform that action at this time.