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

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

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

// 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

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

def fetchPIDE(version: Version)(implicit ec: ExecutionContext): Future[List[Path]] = {
  val repositories = Seq(Repository.ivy2Local, Repository.mavenCentral, Repository.sonatypeReleases)

  val files = coursier.Files(
    Seq("https://" -> new File(sys.props("user.home") + "/.libisabelle/cache")),
    () => sys.error("impossible")
  )

  val cachePolicy = Repository.CachePolicy.Default

larsrh

-- Joke implementation of a joke idea
-- Scala-2.8-style collections in Haskell

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DefaultSignatures #-}

larsrh

theory Scratch
imports Main
begin

fun insert :: "'a::linorder ⇒ 'a list ⇒ 'a list" where
"insert x [] = [x]" |
"insert x (y # ys) = (if x ≤ y then x # y # ys else y # insert x ys)"

inductive sorted :: "'a::linorder list ⇒ bool" where
empty: "sorted []" |