Skip to content

Instantly share code, notes, and snippets.


Stuart Gaλe bishboria

View GitHub Profile

Keybase proof

I hereby claim:

  • I am bishboria on github.
  • I am 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 / LittleLang.agda
Last active Jan 17, 2016
How do I fix the 'cannot decide' error in the opt function?
View LittleLang.agda
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
View custom.css
body {
background: #fff;
color: #000;
#pulls {
text-shadow: unset;
color: #000;
View SingleCaseInduction.agda
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 / ListSyntax.agda
Last active Jan 4, 2016
Using agda mixfix operators to create a better list syntax
View ListSyntax.agda
module ListSyntax where
data : Set where
zero :
succ :
{-# BUILTIN ZERO zero #-}
{-# BUILTIN SUC succ #-}
bishboria / parse_expr.rb
Created Jan 21, 2014
Little Schemer first meeting
View parse_expr.rb
def parse_expr
if $EXPR[0] == "("
def parse_atom
first = [$EXPR.index(' '),$EXPR.index(')'),$EXPR.length].compact.min
bishboria / factorial_list_hylomorphism.rb
Created Nov 1, 2013
Factorial using a list hylomorphism in… Ruby
View factorial_list_hylomorphism.rb
class Pair
attr_reader :fst, :snd
def initialize(fst, snd)
@fst, @snd = fst, snd
# Welp
class Either
attr_reader :val
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
bishboria / two.idr
Last active Dec 15, 2015
Can't unify when trying to prove case_one_proof
View two.idr
module Main
foo : List Int -> List Int
foo xs = if List.length xs < 4
then ?case_one
else ?case_two
Main.case_one = proof {
intro xs;
refine List.reverse;
bishboria / addition_commutativity.idr
Last active Dec 11, 2015
I want type level n + m = m + n. Should Idris' type checker be able to work this out?
View addition_commutativity.idr
-- these definitions give a unification error
add : Nat -> Nat -> Nat
add O y = y
add x O = x
add (S k) y = S (add y k)
-- Can't unify Vect A m with Vect A (add m O)
append : {A:Set} -> Vect A n -> Vect A m -> Vect A (add m n)
append Nil ys = ys