larsrh

// can be used like this:
// addCompilerPlugin("local.whatever" %% "whatever-plugin" % "0.1-SNAPSHOT" classifier "assembly" cross CrossVersion.patch)

name := "whatever-plugin"

organization := "local.whatever"

scalaVersion := "2.12.0"
crossScalaVersions := Seq("2.12.0", "2.12.1", "2.11.8", "2.11.7", "2.11.6")

larsrh

# Uses Alex Archambault's coursier launcher
# Download as follows:
# $ curl -L -o coursier https://git.io/vgvpD && chmod +x coursier
# ... or refer to instructions here: <https://github.com/alexarchambault/coursier>

# list any dependencies here
COURSIER_CLASSPATH="$(coursier fetch -p com.chuusai:shapeless_2.11:2.3.1)"

# this downloads and launches tut in a seperate step
# the 'classpath' argument is being interpreted by scalac

larsrh

// rank 1

type num[a] = (a => a) => a => a

def zero[a]: num[a] = f => x => x
def succ[a](n: num[a]): num[a] = f => x => f(n(f)(x))

def eval(n: num[Int]): Int = n(_ + 1)(0)

// rank 2

larsrh

package test

import org.specs2.Specification
import org.specs2.specification.AfterAll

class TestSpec extends Specification
  with AfterAll { def is = s2"""

  Test spec
  

larsrh

theory Scratch
imports Main
begin

interpretation lifting_syntax .

definition "graph f = (λx y. y = f x)"

lemma graph_map: "list_all2 (graph f) = graph (map f)"
proof (rule ext)+

larsrh

package vanilla

sealed trait Optic[G[_,_] <: Optic[G, _, _], S, A] {
  def compose[F[_, _] <: Optic[F, _, _], B](o: F[A, B])(implicit lub : Lub[G,F]) : lub.T[S, B] =
    lub.compose(self, o)
  def self: G[S,A]
  def desc: List[String]
}

case class Traversal[A,B](desc : List[String]) extends Optic[Traversal,A,B] {

larsrh

// Initial idea courtesy of @dwijnand
// Improved by @fthomas

sealed trait List[+T] {
  def head: Option[T]
}

final case class Cons[T](h: T, t: List[T]) extends List[T] {
  val head: Some[T] = Some(h)
}

larsrh

def ws = manager.build.project.workspace

def web = ws.child("web")

def target = new hudson.FilePath(new java.io.File("/var/www/afp-devel"))
target.mkdirs()
target.deleteContents()

web.copyRecursiveTo(target)

larsrh

import leon.annotation._
import leon.collection._
import leon.lang._

@isabelle.typ(name = "Nat.nat")
sealed abstract class Nat {

  @isabelle.function(term = "op <=")
  def <=(that: Nat): Boolean = this match {
    case Zero() => true

larsrh

scalaVersion := "2.10.3"

libraryDependencies ++= List(
  "com.typesafe.slick" %% "slick" % "2.0.0",
  "com.h2database" % "h2" % "1.3.170"
)