LeifW

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

LeifW

/*
 * 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

-- 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 

LeifW

@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>.
@prefix : <http://linkedrecipes.org/schema/>.
@prefix foaf: <http://xmlns.com/foaf/0.1/>.

<http://www.foodista.com/recipe/J2T4QC7D/pumpkin-chocolate-chip-walnut-cookies> a :Recipe;
  :steps (
    "ONE: Combine pumpkin, sugar, vegetable oil, and egg"
    "TWO: In a separate bowl, stir together flour, baking powder, baking soda, ground cinnamon, and salt. Dissolve the baking soda with the milk, and stir in. Add the flour mixture to the pumpkin mixture and mix well."
    "THREE: Add vanilla, chocolate chips, and walnuts. Mix well."
    "FOUR: Shape and flatten dough on cookie sheet (covered with parchment paper) and bake at 350 degrees for approximately 10 minutes or until lightly brown and firm."