Skip to content

Instantly share code, notes, and snippets.

@LeifW
LeifW / plus_comm.idr
Created January 24, 2016 02:48 — forked from edwinb/plus_comm.idr
plus commutes
plus_comm : (n : Nat) -> (m : Nat) -> (n + m = m + n)
-- Base case
(O + m = m + O) <== plus_comm =
rewrite ((m + O = m) <== plusZeroRightNeutral) ==>
(O + m = m) in refl
-- Step case
(S k + m = m + S k) <== plus_comm =
rewrite ((k + m = m + k) <== plus_comm) in
/*
* This is the Towers of Hanoi example from the prolog tutorial [1]
* converted into Scala, using implicits to unfold the algorithm at
* compile-time.
*
* [1] http://www.csupomona.edu/~jrfisher/www/prolog_tutorial/2_3.html
*/
object TowersOfHanoi {
import scala.reflect.Manifest
@LeifW
LeifW / machines.hs
Last active August 29, 2015 14:04 — forked from pchiusano/machines.hs
-- Type-aligned sequence catenable queue supporting O(1) append, snoc, uncons
-- Don't need it to be a dequeue (unsnoc not needed)
data TCQueue c a b -- c is the category, a is starting type, b is ending type
type Channel f a b = TCQueue (Transition f) a b
type Process f b = Channel f () b
data Transition f a b where
Bind :: (a -> Process f b) -> Transition f a b
OnHalt :: (Cause -> Process f b) -> Transition f a b