Skip to content

Instantly share code, notes, and snippets.


Larry Diehl larrytheliquid

View GitHub Profile
larrytheliquid / Foo.agda
Last active Aug 29, 2015
Positivity checker
View Foo.agda
module Foo where
open import Level using ( Lift )
data : Set where
zero :
suc :
elimℕ : {ℓ} (P : Set ℓ)
(pzero : P zero)
(psuc : (n : ℕ) P n P (suc n))
View bug_walk_simulation_test.rb
module BugWalkSimulation
describe Bug, "#dead?" do
it "should be false when the number of moves is less than the moves lifetime" do
bug = new_bug(:moves_lifetime => 3)
bug.should_not be_dead
it "should be true when the number of moves is greater than the moves lifetime" do
bug = new_bug(:moves_lifetime => 2)
View gist:1b433ee3a36156a9be42
There are a lot of resources to learn from, and it's hard to pick just one. Below are links to learning about dependently typed programming. I think that the most comfortable path is to learn DT programming first, and then learn more of the pure math and type theory behind it along the way as you get more experienced.
Basically, Coq is the most mature and oldest, but is more tedious to do dependently typed programming with.
Agda is not as mature, but it supports dependently typed programming very well.
Idris is an even newer language that also supports dependently typed programming well, and IMO has the best chance of being a practically used language.
Personally, I mostly use Agda.
Software foundations -
Certified programming with dependent types -
View gist:31633
(ns clojure (:use specjure))
(describe + "without arguments"
(it "returns 0"
(should = 0 (+))))
(describe + "with a single argument"
(it "returns the argument"
(should = 1 (+ 1))
(should = 1337 (+ 1337))))
View gist:31635
(ns clojure (:use specjure))
(it + "without arguments returns 0"
(should = (+) 0))
(it + "with a single argument returns the argument"
(should = 1 (+ 1))
(should = 1337 (+ 1337)))
(it + "with multiple arguments returns the sum of the arguments"
View gist:31637
;;; RSpec stack example:
;;; Implementation
(ns specjure.examples
(:refer-clojure :exclude [empty? peek])
(:use specjure))
(defn stack []
(ref ()))
View gist:41468
(share-test "non-empty specjure.examples/stack" []
(test "is not empty"
(is (not (empty? ($get :stack)))))
(test "returns the top item when applied to specjure.examples/peek"
(is (= ($get :last-item-added) (peek ($get :stack)))))
(test "does not remove the top item when applied to specjure.examples/peek"
(is (= ($get :last-item-added) (peek ($get :stack))))
(is (= ($get :last-item-added) (peek ($get :stack)))))
View client.rb
require "rubygems"
require "rack/client"
require "rack/contrib"
puts "PUT'ing /store/fruit (with strawberry)"
Rack::Client.put "http://localhost:9292/store/fruit", "strawberry"
puts "GET'ing /store/fruit"
View gist:151724
# tail.rb
# JAVA_OPTS="-Djruby.tailcall.enabled=true" jruby tail.rb --1.9
# Error: Your application used more stack memory than the safety cap of 1024k.
# Specify -J-Xss####k to increase it (#### = cap size in KB).
# Specify -w for full StackOverflowError stack trace
def fact(n, acc)
if n == 0
View gist:177894
require 'rubygems'
require 'eventmachine'
require 'em-http'
require 'dataflow' {{}
module EventMachine