einblicker

object Formatter {
  sealed abstract class Dir[A] {
    def formatAux: String => A
    def format: A = formatAux.apply("")
  }

  case object E extends Dir[String] {
    def formatAux = identity
  }

einblicker

interface Func<A, B> {
  B apply(final A arg);
}

abstract class Dir<A, B> {
  public Dir() {}
  abstract public Func<Func<String, A>, Func<String, B>> format();
}

class DLit<A> extends Dir<A, A> {

einblicker

object TypesafeFormatter {
  sealed abstract class Dir[A, B] {
    def format : (String => A) => (String => B)
  }
  def l[A](s: String): Dir[A, A] = L[A](s)
  case class L[A](s: String) extends Dir[A, A] {
    def format = {
      (cont: String => A) =>
        (out: String) =>
          cont(out + s)

einblicker

Section List_J.

Module NatList.

Inductive natprod : Type :=
  pair : nat -> nat -> natprod.

Definition fst (p : natprod) : nat :=
  match p with
  | pair x y => x

einblicker

require 'continuation'

def shift
  callcc {|c1| $ctn.(yield(proc {|v| callcc {|c2| $ctn = c2; c1.(v) } })) }
end

def reset
  callcc {|c| $ctn = c; v = yield; $ctn.(v) }
end

einblicker

object ParityBit {
  type B = Int
  def f(x1: B, x2: B, x3: B, x4: B) =
    (x1 ^ x2 ^ x3,
     x1 ^ x2 ^ x4,
     x2 ^ x3 ^ x4)

  def g(x1: B, x2: B, x3: B, x4: B)(
    c1:B, c2:B, c3:B
  ) = 

einblicker

Section Basics_J.

Definition nandb (b1 b2 : bool) : bool :=
 match (b1, b2) with
 | (false, _) => true
 | (_, false) => true
 | _ => false
 end.

Example test_nandb1: (nandb true false) = true.

einblicker

Section CPDT_Exercise_5.

Section Tree.

Variable A : Set.

CoInductive tree :=
 | Node : A -> tree -> tree -> tree.

CoInductive tree_eq : tree -> tree -> Prop :=

einblicker

Section CPDT_Exercise_4_6.

(* problem 1 *)
Variable P Q R : Prop.

Goal (True \/ False) /\ (False \/ True).
Proof.
split; [ left | right ]; apply I.
Qed.

einblicker

(define (mark e)
  (let loop ((e e) (envs '()))
    (match
     e
     (('lambda args es ...)
      `(lambda ,args ,@(map (cut loop <> (cons args envs)) es)))
     ((? symbol? s)
      (cond
       ((find
	 (lambda (e) (memq s e))