einblicker

object Vec {
  object NotEq {
    class =!=[A, B]
    implicit def aNeqB[A, B] = new =!=[A, B]
    implicit def aNeqA1[A] = new =!=[A, A]
    implicit def aNeqA2[A] = new =!=[A, A]
  }
  
  object Nat {
    sealed trait Nat {

einblicker

object Proof {
  type Not[A] = A => Nothing

  trait All[P[_]] {
    def apply[A]: P[A]
  }

  def DN[A](p: Not[Not[A]]): A =
    p(return (_: A))

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

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

Section CPDT_Exercise_5.

Section Tree.

Variable A : Set.

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

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

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

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

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

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

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)