exterm

# add to config/boot.rb

require "benchmark"

$require_nesting = -1

def require(file_name)
  result = nil

  $require_nesting += 1

exterm

Spaghetti Bolognese alla mamma

Ingredients

• 500g Spaghetti
• 1 Onion
• 1 Carrot
• 1 Celery
• 1 Garlic
• 1/2 Cup Red Wine

exterm

Keybase proof

I hereby claim:

• I am exterm on github.
• I am exterm (https://keybase.io/exterm) on keybase.
• I have a public key ASDIWLjI0H0bvrlQlldvxKJErZcPYUOAt_P6NFla7Ay6bgo

To claim this, I am signing this object:

exterm

/tmp$ dart --version
Dart VM version: 0.8.5.1_r28990 (Tue Oct 22 04:50:58 2013) on "linux_x64"

/tmp$ dartanalyzer test.dart 
Analyzing test.dart...
No issues found

/tmp$ dart -c test.dart 
Unhandled exception:
type 'int' is not a subtype of type 'double' of 'x'.

exterm

# Contributor: Moritz Heidkamp <moritz@twoticketsplease.de>
pkgname=emacs-haml-mode-git
pkgver=20110912
pkgrel=1
pkgdesc="An emacs mode for editing HAML code."
arch=("i686" "x86_64")
url="http://haml-lang.com/"
license=('MIT')
makedepends=('git')
provides=(emacs-haml-mode)

exterm

%% multi clause function type spec

-spec plus(integer(), float())   -> float();
          (float(),   integer()) -> float();
          (float(),   float())   -> float();
          (integer(), integer()) -> integer().
plus(A,B) ->
    A + B.

testp() ->

exterm

{-@ error2 :: {v: String | false } -> a  @-}
error2     :: String -> a
error2     = error

-- a program using this function typechecks exactly when LiquidHaskell can prove that the
-- function error2 is never called.

exterm

data Vec (A : Set) : Nat -> Set where
  [] : Vec A zero
  _::_ : {n : Nat} -> A -> Vec A n -> Vec A (succ n)




head : {A : Set} {n : Nat} -> Vec A (succ n) -> A
head (x :: _) = x

exterm

data PList a b = Nil
               | Cons a (PList a b)

test :: PList Int String
test = Cons 3 $ Cons 2 $ Cons 1 Nil

data Foo = Foo

test2 :: PList Int Foo
test2 = Cons 3 $ Cons 2 $ Cons 1 Nil

exterm

data Safe a = Safe a
data NotSafe = NotSafe
data SafeList a b where
  Nil :: SafeList a NotSafe
  Cons :: a -> SafeList a b -> SafeList a (Safe b)


safeHead :: SafeList a (Safe b) -> a
safeHead (Cons x _) = x
-- safeHead Nil = ???