jroesch

Require List Common. 

Import Common. 

Open Scope list_scope. 

(** Heterogeneous lists, aka tuples, aka type-indexed lists. *)
Notation "[ ]" := nil : list_scope.
Notation "t :: q" := (cons t q) : list_scope. 

jroesch

module HTT

data One = MkOne

pr1 : (a, b) -> a
pr1 (x, _) = x

pr2 : (a, b) -> b
pr2 (_, y) = y

jroesch

package object As {
  import shapeless._
  import syntax.typeable._
  import syntax.std.traversable._
  import ops.traversable._
  
  implicit def asOps[A](xs: List[A]) = new AsOps(xs)

  final class AsOps[A](xs: List[A]) {
    def as[U](implicit as: As[U]): Option[U] = as.apply(xs)

jroesch

module Example

data Result i r = Fail String
                | Done i r 

data ExType i a = MkExType (r : Type ** a -> Result i r)

fail : {t : Type} -> String -> ExType i a
fail {t} s = MkExType (t ** (\x => Fail "bleh"))

jroesch

{-# LANGUAGE RankNTypes #-}
data Result i r = Fail String
                | Done i r 

data ExType i a = ExType { extract :: forall r. a -> Result i r }

fail :: String -> ExType i a
fail s = ExType (\x -> Fail "bleh")

jroesch

typeOf : {A : Type} -> (a : A) -> Type
typeOf {A} _ = A

jroesch

#include <fstream>

using namespace std;

void print2Dot(elem *elm) {
    std::fstream fs;
    int count = 0;
    fs << "diagraph G {" << endl
    fs.open("output.dot", std::fstream::out)
    recursePrint2Dot(0, fs, elm);

jroesch

def Object.finalize_with(*ivars_names, &block)
  old_init = instance_method(:initialize)

  define_method :initialize do |*args|
    puts "MyBlock: #{block}"
    old_init.bind(self).call(*args)
    ivars = ivars_names.map { |ivar| instance_variable_get(ivar) }
    ObjectSpace.define_finalizer(self, proc { block.call(*ivars) })
  end
end

jroesch

module Lattice where

data Nat : Set where
    Z : Nat
    S : Nat -> Nat

data Lattice : Set where
    Lo : Lattice
    Hi : Lattice

jroesch

;; -*- coding: utf-8 -*-
(require 'package)

(setq package-archives '(("gnu" . "http://elpa.gnu.org/packages/")
                         ("marmalade" . "http://marmalade-repo.org/packages/")
                         ("melpa" . "http://melpa.milkbox.net/packages/")))

(package-initialize)

; Remove the pesk + ugly toolbar