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.

takeouchida

module Main where

import Control.Monad (mapM_)
import Control.Arrow ((***))
import Data.List (find, sort)
import Data.Maybe (maybe)
import Test.HUnit (Test(..), runTestTT, (~=?))

findTetroid :: [Int] -> Char
findTetroid = match . normalize . toCoord

takeouchida

module Main where

import Control.Monad.Free

data Option a = Some a | None
  deriving Show

instance Functor Option where
  fmap f (Some a) = Some (f a)
  fmap f None = None

takeouchida

module Main where

import Control.Arrow (first)
import Data.Char (isUpper, isLower, toUpper)
import Data.List (tails, maximumBy, findIndex)
import Data.Ord (comparing)
import Data.Maybe (fromMaybe)
import Test.HUnit (Test(..), runTestTT, (~=?))

type Chair = Maybe Char

takeouchida

package sandbox;

import java.util.HashSet;
import java.util.Set;

enum 音 {
  猫の鳴き声, 犬の鳴き声, ツクツクホウシの鳴き声 // などなど...
}

interface 聞く者 {

takeouchida

o = length $ return undefined
s = succ
d n = n + n
main = putStrLn $ map toEnum
  [ d $ d $ d $ s $ d $ d $ d o
  , s $ d $ d $ s $ d $ d $ d $ s $ d o
  , d $ d $ s $ d $ s $ d $ d $ s $ d o
  , d $ d $ s $ d $ s $ d $ d $ s $ d o
  , s $ d $ s $ d $ s $ d $ s $ d $ d $ s $ d o
  , d $ d $ d $ d $ d o

takeouchida

Require Import List Arith ZArith Program.

Class Monoid {A} (dot : A -> A -> A) (zero : A) := {
  monoid_1st_law : forall a, dot a zero = a;
  monoid_2nd_law : forall a, dot zero a = a;
  monoid_3rd_law : forall a b c, dot (dot a b) c = dot a (dot b c)
}.

Instance nat_plus_Monoid : Monoid plus 0.
  split; auto with arith.