larsrh

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

object Lists {

  @isabelle.script(
    name = "Safe_Head",
    source = """

larsrh

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}

module Terminal where

import Control.Monad.Free (Free, liftF, iterM)
import Control.Monad.State
import Data.Functor.Coyoneda (Coyoneda (Coyoneda), liftCoyoneda)

larsrh

module Hello where

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

infix 4 _≡_

sym : {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

larsrh

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}

data VarKind t = Bound | Free t

larsrh

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Data.HList (

larsrh

> quickCheckResult False
*** Failed! Falsifiable (after 1 test):  
Failure {numTests = 1, numShrinks = 0, numShrinkTries = 0, numShrinkFinal = 0, usedSeed = TFGenR 000000025E37A9D3000000000003D090000000000000DE920000005C5B22D280 0 8 4 0, USEDSIZE = 0, REASON = "FALSIFIABLE", THEEXCEPTION = NOTHING, LABELS = [], OUTPUT = "*** FAILED! FALSIFIABLE (AFTER 1 TEST): \N"}

larsrh

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

larsrh

haskell-src-exts

• incomplete Unicode support (report)

postgresql-simple

• ByteString is not treated as binary data by default (report, report)

larsrh

$ sbt -no-share -sbt-create # paulp's launcher script
Getting org.scala-sbt sbt 0.13.5 ...
downloading http://repo.typesafe.com/typesafe/ivy-releases/org.scala-sbt/sbt/0.13.5/jars/sbt.jar ...
        [SUCCESSFUL ] org.scala-sbt#sbt;0.13.5!sbt.jar (857ms)
downloading http://repo1.maven.org/maven2/org/scala-lang/scala-library/2.10.4/scala-library-2.10.4.jar ...
        [SUCCESSFUL ] org.scala-lang#scala-library;2.10.4!scala-library.jar (3166ms)
downloading http://repo.typesafe.com/typesafe/ivy-releases/org.scala-sbt/main/0.13.5/jars/main.jar ...
        [SUCCESSFUL ] org.scala-sbt#main;0.13.5!main.jar (2354ms)
downloading http://repo.typesafe.com/typesafe/ivy-releases/org.scala-sbt/compiler-interface/0.13.5/jars/compiler-interface-src.jar ...
        [SUCCESSFUL ] org.scala-sbt#compiler-interface;0.13.5!compiler-interface-src.jar (798ms)

larsrh

scalaVersion := "2.10.3"
 
libraryDependencies ++= Seq(
  "org.scalaz" %% "scalaz-core" % "7.1.0-M6",
  "org.scalaz" %% "scalaz-effect" % "7.1.0-M6"
)