This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
val result = for { | |
i <- 100.set("Hello") | |
j <- 100.set("World") | |
} yield i + j | |
result.value assert_=== ("HelloWorld", 200) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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)) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(defprotocol Action | |
(action [this e])) | |
(deftype Controller [^{:unsynchronized-mutable true} label] | |
Action | |
(action [this e] | |
(.setText label "Action!"))) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
trait Foo | |
type Bar = Int @@ Foo |