lenary

#include <dlfcn.h>
#include <stdio.h>
#include <stdbool.h>
#include <string.h>

#ifdef __APPLE__
#include <mach-o/dyld.h>
#else // Linux
#include <link.h>
#endif

lenary

-- In `f` we want to keep piping (part of) the result of one function into
-- another, and stop as soon as something fails
f :: [A] -> Either String (B, [A])
f xs =
  case f1 xs of
    Left s -> Left s
    Right (res1, xs') ->
      case f2 xs' of
        Left s -> Left s
        Right (res2, xs'') ->

lenary

%% Source Code Notes
\ProvidesPackage{listing-label}
% We use tikz for drawing the circles around the letters. Dumb, probably. 
\RequirePackage{tikz}

% Counter, numbered by section
\newcounter{lstlistinglabel}[section]
% Length for left out-dent
\newlength{\lstlabelleftoutdent}

lenary

#include <stdio.h>

// The file with the unchecked interface
#include <stdlib.h>

// The Redeclaration with the correct type
void *calloc(size_t nmemb, size_t size) : byte_count(nmemb * size);

#pragma BOUNDS_CHECKED ON

lenary

{-# OPTIONS --copatterns #-}

open import Agda.Builtin.Nat
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality


trans : {A : Set} {a b c : A} -> a ≡ b -> b ≡ c -> a ≡ c
trans refl refl = refl

lenary

{-# OPTIONS --copatterns #-}

open import Agda.Builtin.Nat

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

record Stream (A : Set) : Set where
  coinductive

lenary

$ racket -iq -e "(require rosette)"
Welcome to Racket v6.4.
> (define (foo) identity)
> foo
#<procedure:foo>
> identity
#<procedure:identity>
> ((foo) 3)
free-identifier=?: contract violation
  expected: identifier?

lenary

$ erl
Erlang R15B03 (erts-5.9.3.1) [source] [64-bit] [smp:4:4] [async-threads:0] [hipe] [kernel-poll:false] [dtrace]

Eshell V5.9.3.1  (abort with ^G)
1> <<99,111,110,118,101,114,115,97,116,105,111,110>>.
<<"conversation">>
2> <<100,107,114,100,54,58,104,107,110,120,110,114,115,49>>.
<<"dkrd6:hknxnrs1">>

lenary

bind-key -temacs-copy c copy-selection
bind-key -temacs-copy x copy-pipe "reattach-to-user-namespace /usr/bin/pbcopy"
bind-key -temacs-copy z copy-pipe "mate"

lenary

Counters are expected to land in Riak 1.4! See this pull-request.

h/t to @russelldb for the demo code.