mrb

(ns chords.core
  (:refer-clojure :exclude [==])
  (:require [clojure.core.logic :refer :all]
            [clojure.core.logic.fd :as fd]
            [clojure.core.logic.pldb :as pldb]
            [fipp.edn :refer (pprint) :rename {pprint fipp}]))

(pldb/db-rel note-name ^:index p)
(pldb/db-rel octave ^:index p)
(pldb/db-rel note ^:index p1 ^:index p2)

mrb

(ns peanoo.core
  (:refer-clojure :exclude [==])
  (:require [clojure.core.logic :as l]
            [clojure.core.logic.fd :as fd]))

(defn fdin 
  [v f c]
  (fd/in v (fd/interval f c)))

(defn in-interval

mrb

instance (Ord k, Arbitrary k, Arbitrary v) => Arbitrary (Map k v) where
  arbitrary = Data.Map.fromList <$> arbitrary
  shrink m = Data.Map.fromList <$> shrink (Data.Map.toList m)

mrb

module Chain where

import Data.Map.Strict(Map,insertWith,empty,member,(!))
import System.Random(randomRIO)

data Chain = Chain (Map String [String]) Int deriving (Show)

build :: [String] -> [String] -> Chain -> Chain
build []  _ chain = chain
build [_] _ chain = chain

mrb

module DNA where

hammingDistance :: String -> String -> Integer
hammingDistance f s = sum (zipWith (\x y -> case x == y of {True -> 0; False -> 1}) f s)

mrb

mrb and Maya are moving!*

Come say goodbye! Sunday 7/27 @ 9PM

Washington Commons, Brooklyn, NY

* To College Park, MD - for now

mrb

module FizzBuzzC

%default total

-- Dependently typed FizzBuzz, constructively

-- A number is fizzy if it is evenly divisible by 3
data Fizzy : Nat -> Type where
  ZeroFizzy : Fizzy 0
  Fizz : Fizzy n -> Fizzy (3 + n)

mrb

module Main
 
import Prelude.Algebra

record GCounter : Type where
  MkGCounter : (value : Nat) -> GCounter

gcjoin : GCounter -> GCounter -> GCounter
gcjoin l r = (MkGCounter (maximum (value l) (value r)))

mrb

total maximumSucc : (l : Nat) -> maximum (S l) l = (S l)
maximumSucc Z = refl
maximumSucc (S l) = rewrite maximumSucc l in refl

mrb

module Main
 
import Prelude.Algebra

record GCounter : Type where
  MkGCounter : (value : Nat) -> GCounter

natMax : Nat -> Nat -> Nat
natMax Z m = m
natMax (S n) Z = S n