View gist:4cb4f415001f0bf517c4
1 2 3 4 5 6 7 8 9 10
import spray.json._
import DefaultJsonProtocol._
 
case class Color(name: String, red: Int, green: Int, blue: Int)
 
object MyJsonProtocol extends DefaultJsonProtocol {
implicit val colorFormat = jsonFormat4(Color)
}
 
object Main {
View gist:68aec1ee21ad2f67e594
1 2 3 4 5 6 7 8 9
MacBook-Pro:ermine-scala joshcough$ ./sbt
Detected sbt version 0.13.5
Starting sbt: invoke with -help for other options
:ownloading sbt launcher 0.13.5
From http://typesafe.artifactoryonline.com/typesafe/ivy-releases/org.scala-sbt/sbt-launch.jar3.5
/sbt-launch.jar0.13.5
/sbt-launch.jar. Obtain the jar manually and place it at ./.lib/0.13.5
MacBook-Pro:ermine-scala joshcough$ ls .lib/
0.13.5 0.13.5?
View gist:953a54ae0b3f68486a5a
1 2 3 4 5 6 7 8 9 10
module Infer where
 
import Control.Monad.State
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
 
data Var = V {-# UNPACK #-} !Int (Maybe String)
 
data HM = HM
{ nextVar :: {-# UNPACK #-} !Int
View gist:a2cbf0bb24ce7575ff9a
1 2 3 4
def sender[T](addr:InetSocketAddress, p: Process[Nothing,T])(implicit c: Codec[T]): Process[Task, ByteVector] = {
val encoder : Process1[T,ByteVector] =scodec.stream.encode.many(c).encoder.map(_.toByteVector)
tcp.connect(addr)(tcp.lift(p.toSource |> encoder))
}
View CodecQuestion
1 2 3 4 5 6 7 8 9 10
Code:
 
import scodec._
import scodec.bits._
import codecs._
import scalaz._
import Scalaz._
 
object Messages {
sealed trait MessageType
View gist:b0385b3c4a02515a82dc
1 2 3 4 5 6 7 8 9 10
RET (translated from <return>) runs the command newline, which is an
interactive compiled Lisp function in `simple.el'.
 
It is bound to RET.
 
(newline &optional ARG INTERACTIVE)
 
Insert a newline, and move to left margin of the new line if it's blank.
If option `use-hard-newlines' is non-nil, the newline is marked with the
text-property `hard'.
View plus_n_n_injective.v
1 2 3 4 5 6 7 8 9 10
(* This black magic proof should be referred back to a lot.
important to note that intros moves LHS from the goal to the context.
somehow I didn't understand that completely, all this time.
*)
Theorem plus_n_n_injective : forall n m,
n + n = m + m ->
n = m.
Proof.
intros n. induction n as [| n'].
(* question: how can we just destruct m, if we haven't introduced it?
View gist:2a1cb023293d6a6f56d8
1 2 3 4 5 6 7 8 9 10
interpE (PrimE p) = interpE l where
a = App (PrimE p) [Var (B 0), Var (B 1)]
l = Lambda [Variable "x", Variable "y"] (abstract (^? _B) a)
 
src/L/L5/L5Interp.hs:60:39:
Could not deduce (a ~ Var Int a0)
from the context (MonadHOComputer c m (L5Runtime a))
bound by the type signature for
interpE :: (MonadHOComputer c m (L5Runtime a)) =>
E a -> m (L5Runtime a)
View gist:e2e98d6c76431550f1ed
1 2 3 4 5 6
go f pe@(PrimE p) = go (unvar (args !!) f) y where
v = Variable
args :: [Variable]
args = primVars p
y :: L5.E (Var Int a)
y = Lambda [v "x", v "y"] (abstract (^? _B) (App (PrimE p) [Var (B 0), Var (B 1)]))
View gist:53e3b48e2e07f17f4786
1 2 3 4 5 6 7 8
instance (Eq a, FromSExpr a) => FromSExpr (E a) where
fromSExpr (List [AtomSym "lambda", List args, b]) = do
e <- fromSExpr b
as <- sequence $ fmap fromSExpr args
return $ Lambda (length args) $ abstract (flip elemIndex as) e
--if wellFormedArgList args
-- then return $ Lambda (length args) $ abstract (flip elemIndex as) e
-- else fail $ "bad arguments" ++ show args -- fail if args is ill formed
Something went wrong with that request. Please try again.