Skip to content

Instantly share code, notes, and snippets.

Stuart Gaλe bishboria

Block or report user

Report or block bishboria

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
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
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/^/ /"'
@bishboria
bishboria / springer-free-maths-books.md
Last active Aug 25, 2019
Springer made a bunch of books available for free, these were the direct links
@bishboria
bishboria / childhood-animated-stuff.md
Last active Aug 31, 2015
Animated stuff when growing up
View childhood-animated-stuff.md

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
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"; \
fi
if test -z "$(vagrant box list | grep -w opengenera)" ; then \
make ubuntu-7.10-server-amd64.box; \
vagrant box add opengenera ubuntu-7.10-server-amd64.box; \
fi
if test -z "$(which veewee)" ; then \
echo "### need to install veewee"; \
You can’t perform that action at this time.