Skip to content

Instantly share code, notes, and snippets.

View bishboria's full-sized avatar

Stuart Gaλe bishboria

View GitHub Profile
@bishboria
bishboria / SingleCaseInduction.agda
Created March 23, 2014 10:49
Single case induction
module SingleCaseInduction where
-- Usual definition of ℕ
data N : Set where
z : N
s : N N
-- Single case definition of ℕ
data _+_ (A : Set) (B : Set) : Set where
@bishboria
bishboria / keybase.md
Created September 24, 2014 13:19
keybase

Keybase proof

I hereby claim:

  • I am bishboria on github.
  • I am bishboria (https://keybase.io/bishboria) on keybase.
  • I have a public key whose fingerprint is 4243 FB55 3364 0BE8 D08E 876F 078A 4BBA 842F C1A0

To claim this, I am signing this object:

@bishboria
bishboria / childhood-animated-stuff.md
Last active August 31, 2015 09:43
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
(define (my-for-each proc list-of-values)
(cond ((null? list-of-values) #t)
(else (proc (car list-of-values))
(my-for-each proc (cdr list-of-values)))))
;; or
(define (my-for-each proc list-of-values)
(if (null? list-of-values)
#t
@bishboria
bishboria / 2011-04-26-intial-SchemeOO.scm
Created April 26, 2011 22:37
Original attempt at OO with Scheme
(define (person person-name person-age)
(define (name)
person-name)
(define (age)
person-age)
(lambda (selector)
(cond ((equal? selector 'name) (name))
((equal? selector 'age) (age))
(#t '(I cant do that Dave!)))))
;; All the OO stuff
(define (object selector-names . all-selectors)
(define (apply-it selector selector-names selectors parameters)
(cond ((null? selectors) '(I cant do that Dave!))
((equal? selector (car selector-names)) (apply (car selectors) parameters))
(#t (apply-it selector (cdr selector-names) (cdr selectors) parameters))))
(lambda (selector . parameters)
(apply-it selector selector-names all-selectors parameters)))
;; Defining a new object type
@bishboria
bishboria / LittleLang.agda
Last active January 17, 2016 16:15
How do I fix the 'cannot decide' error in the opt function?
module LittleLang where
open import Data.Bool
open import Data.Nat
data type : Set where
tNat tBool : type
data exp : type Set where
nat : exp tNat
@bishboria
bishboria / git-stashes.sh
Created February 21, 2016 08:45
Find all git stashes
find . -iname .git | xargs -I % sh -c 'cd %/..; pwd; git stash list | sed "s/^/ /"'
; 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 / multiplication.agda
Last active October 23, 2016 13:14
Exercise: Encode multiplication as a type in 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