takeouchida

import Data.List (foldl', intercalate)
import Test.HUnit (Test(..), runTestTT, (~=?))

process :: String -> String
process = intercalate "," . map show . take 10 . foldl' transf [1..]

isSquare n = let x = sqrt (fromIntegral n) in x - fromIntegral (floor x) == 0

--isCube n = let x = (fromIntegral n) ** (1 / 3) in x - fromIntegral (floor x) == 0
isCube n = round (fromIntegral n ** (1 / 3)) ^ 3 == n

takeouchida

Inductive term : Type :=
  | Ttrue : term
  | Tfalse : term
  | Tifthenelse : term -> term -> term -> term.

Inductive evaluate : term -> term -> Prop :=
  | Eiftrue : forall t2 t3, evaluate (Tifthenelse Ttrue t2 t3) t2
  | Eiffalse : forall t2 t3, evaluate (Tifthenelse Tfalse t2 t3) t3
  | Eif : forall t1 t1' t2 t3, evaluate t1 t1' -> evaluate (Tifthenelse t1 t2 t3) (Tifthenelse t1' t2 t3).

takeouchida

Inductive term : Type :=
  | Ttrue : term
  | Tfalse : term
  | Tifthenelse : term -> term -> term -> term.

Inductive evaluate : term -> term -> Prop :=
  | Eiftrue : forall t2 t3, evaluate (Tifthenelse Ttrue t2 t3) t2
  | Eiffalse : forall t2 t3, evaluate (Tifthenelse Tfalse t2 t3) t3
  | Eif : forall t1 t1' t2 t3, evaluate t1 t1' -> evaluate (Tifthenelse t1 t2 t3) (Tifthenelse t1' t2 t3).

takeouchida

Inductive term : Type :=
  | Ttrue : term
  | Tfalse : term
  | Tifthenelse : term -> term -> term -> term.

Inductive evaluate : term -> term -> Prop :=
  | Eiftrue : forall t2 t3, evaluate (Tifthenelse Ttrue t2 t3) t2
  | Eiffalse : forall t2 t3, evaluate (Tifthenelse Tfalse t2 t3) t3
  | Eif : forall t1 t1' t2 t3, evaluate t1 t1' -> evaluate (Tifthenelse t1 t2 t3) (Tifthenelse t1' t2 t3).

takeouchida

package clientwithproxy

import akka.util.Timeout
import spray.can.Http.ClientConnectionType

import scala.util.{Success, Failure}
import scala.concurrent.duration._
import akka.actor.ActorSystem
import akka.pattern.ask
import akka.event.Logging

takeouchida

import os
import traceback

# Write a message to /var/log/hoge.log
os.system("echo `date '+%Y/%m/%d %H:%M:%S.%N'` 'Some message' >> /var/log/hoge.log")

# Write a traceback to /var/log/hoge.log
os.system("echo `date '+%Y/%m/%d %H:%M:%S.%N'` '" + traceback.format_exc() + "' >> /var/log/hoge.log")

takeouchida

import Control.Applicative ((<$>), (<$), (<*>), (<*), (*>))
import Prelude hiding (null)
import Text.Parsec hiding (string)
import Text.Parsec.Language (javaStyle)
import qualified Text.Parsec.Token as P

data Value = S String | N Double | O [(String, Value)] | A [Value] | B Bool | Null deriving Show

lexer = P.makeTokenParser javaStyle
symbol = P.symbol lexer

takeouchida

module Lookup where

import Prelude hiding (lookup)

lookup :: a -> [(a, b)] -> Maybe b  -- valid if the type a is a kind of Eq instances
lookup k [] = Nothing
lookup k ((k', v):ls) = if k == k' then Just v else lookup k ls

takeouchida

_Main_mainzuzdszdwa_info:
Lc2q2:
        addq $40,%r12
        cmpq 144(%r13),%r12
        ja Lc2q7
        cmpq $100,%r14
        jg Lc2qb
        movq %rsi,%rax
        addq %r14,%rax
        incq %r14 

takeouchida

Require Import Div2.

Theorem div2_double : forall x, div2 (double x) = x.
intro x.
induction x.
  reflexivity.

  unfold double.
  unfold double in IHx.
  rewrite plus_Sn_m.