pirapira

(**
   IOtt functor from
   Swierstra, Wouter, and Thorsten Altenkirch. "Beauty in the Beast."
   In Proceedings of the ACM SIGPLAN Workshop on Haskell Workshop.
   Haskell '07. ACM, 2007. http://doi.acm.org/10.1145/1291201.1291206.
**)

Require Import Logic.FunctionalExtensionality.

Inductive IOtt (a: Set) : Set :=

pirapira

UNSORTED = "/Users/yh/unsorted.txt"

require "shell"
require "find"



def emit(path)
  s = Shell.new
  s.cd path

pirapira

async_core.mli: 
deferred.mli: value to be determined later (that forms monad) / enable choose mechanism
clock.mli:  defer until certain times

typed_tcp.mli: would be fun to use

writer.mli: reducing number of write() calls


#use "topfind";;

pirapira

import java.io.*;
import java.io.BufferedWriter;
import java.text.*;
import java.util.*;
import javax.sound.sampled.*;

public class AudioInput implements Runnable{

	public static void main(String args[]) {
		AudioInput audioinput = new AudioInput();

pirapira

#! /usr/local/bin/ruby
require 'net/http'
Net::HTTP.version_1_2

begin
  r = Net::HTTP.start('example.com', 80) {|http|
        res = http.get('/directory/file')
      }
rescue
  system('echo "NG" | mail -c addr@example.com -s "server faillure" addr2@example.com')

pirapira

Parameter person :Set.
Parameter thing: Set.
Parameter bottle: thing.
Parameter own: person -> thing -> Prop.

Parameter capitalist: forall (x: thing), { p:person & own p x }.

Definition owner: person.
generalize (capitalist bottle).
intros.

pirapira

Parameter person thing : Set.

Parameter own: person -> thing -> Prop.

Parameter capitalist: forall (x: thing), exists p:person, own p x.

Parameter bottle: thing.

Definition owner: person.
Admitted.

pirapira

Require Import ConCaT.CATEGORY_THEORY.FUNCTOR.Functor.


Section alg_def.

Variables (A : Category) (T : Functor A A).

Structure Alg_ob : Type := {Ob_alg_ob : A; Mor_alg_ob  : T Ob_alg_ob --> Ob_alg_ob}.

 Section alg_arrow_def.

pirapira

function-data/relation mapper

スキーマ

table mail {
    id int primary key,
    from_addr varchar[50],
    date datetime,
    mailbox varchar[50]

}

pirapira

require 'rubygems'
require 'grit'
include Grit

repo = Repo.new(".")

def date(head)
   head.commit.committed_date
end