Skip to content

Instantly share code, notes, and snippets.

val result = for {
i <- 100.set("Hello")
j <- 100.set("World")
} yield i + j
result.value assert_=== ("HelloWorld", 200)
val s = for {
i <- init[Int]
_ <- modify[Int](_ |+| 5)
j <- gets[Int, Int](_ |+| 5)
} yield i |+| j
s ! 0 assert_=== 10
s ! 5 assert_=== 20
lazy val f: Kleisli[Option, Int, String] = kleisli(5.shows +>: _.shows.some)
f(5) assert_=== Some("55")
lazy val g: Kleisli[Option, String, Int] = ☆(_.parseInt.toOption)
g("5") assert_=== Some(5)
@halcat0x15a
halcat0x15a / mathgirl.v
Created January 9, 2012 22:14
Coqの練習だよ。
Inductive P : Set :=
I : P
| PS : P -> P.
Fixpoint Padd (n m : P) : P :=
match n with
| I => PS m
| PS n' => PS (Padd n' m)
end.
Inductive P : Set :=
I : P
| PS : P -> P.
Fixpoint Padd (n m : P) : P :=
match n with
| I => PS m
| PS n' => PS (Padd n' m)
end.
object CoqMain {
object CoqModule {
sealed abstract class Nat
case class Zero() extends Nat
case class Succ(x1: Nat) extends Nat
def nat_rect[A] : (A => ((Nat => (A => A)) => (Nat => A))) = {
(f:A) => (f0:(Nat => (A => A))) => (n:Nat) =>
n match {
case Zero() => f
case Succ(n0) => f0(n0)(nat_rect(f)(f0)(n0))
@halcat0x15a
halcat0x15a / gist:1670501
Created January 24, 2012 14:44
ぼくのかんがえたさいきょうのしぜんすう
trait Nat {
type Plus[N <: Nat] <: Nat
def +[N <: Nat](n: N): Plus[N]
type Mult[N <: Nat] <: Nat
def *[N <: Nat](n: N): Mult[N]
def toInt: Int
}
case object Zero extends Nat {
type Plus[N <: Nat] = N
sealed trait SList {
type Self <: SList
type Function[A]
def apply[A](f: Function[A]): A
def ::[A](a: A) = SCons(a, this.asInstanceOf[Self])
}
case object SNil extends SList {
type Self = SNil.type
type Function[A] = A
(defprotocol Action
(action [this e]))
(deftype Controller [^{:unsynchronized-mutable true} label]
Action
(action [this e]
(.setText label "Action!")))
trait Foo
type Bar = Int @@ Foo