notogawa

import Control.Monad
import Data.List

main :: IO ()
main = interact $ format . solve . read

format :: [[Int]] -> String
format = unlines . map (unwords . map show)

solve :: Int -> [[Int]]

notogawa

// tarai.cpp
// $ g++ -o tarai -O2 -std=C++0x tarai.cpp
#include <iostream>
#include <cstdlib>
#include <functional>

int tarai(int x, int y, int z) {
    return (x <= y)
        ? y
        : tarai(tarai(x - 1, y, z),

notogawa

module ABC011A where

open import IO
open import Function
open import Coinduction
open import Data.String using (String)

nextMonthOf : String → String
nextMonthOf "1"  = "2"
nextMonthOf "2"  = "3"

notogawa

module PO where

open import Level
open import Relation.Binary
open import Data.Product

module Propaties {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_≤_ : Rel A ℓ₂} (po : IsPartialOrder _≈_ _≤_ ) where

  data lower-bound-of_is_ (P : A → Set ℓ₂) : A → Set (a ⊔ ℓ₂) where
    lb : ∀ {x} → P x → (∀ x' → P x' → x ≤ x') → lower-bound-of P is x

notogawa

module FoldZipFusion {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} (_⊕_ : A → B → B) (_⊗_ : C → D → A)where

open import Function
open import Data.List
open import Relation.Binary.PropositionalEquality

_⊛_ : {z : B} → C → (List D → B) → List D → B
_⊛_ {z} x k [] = z
_⊛_ {z} x k (y ∷ ys) = (x ⊗ y) ⊕ k ys

notogawa

module Test where

open import Function
open import Data.Empty
open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.DivMod using (_divMod_; _mod_; result)
open import Data.Fin using (zero; suc; toℕ)
open import Data.Sum
open import Data.Product

notogawa

open import Category.Monad

module DoLikeNotation {l M} (monad : RawMonad {l} M) where

open RawMonad monad

bind-syntax = _>>=_

syntax bind-syntax F (λ x → G) = ∣ x ← F ∣ G

notogawa

module Test where

open import Relation.Binary.PropositionalEquality

postulate
  extensionality : ∀ {a} {b} {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g

covariant : {B : Set} → (B → B → B) → {A : Set} → (A → B) → (A → B) → (A → B)
covariant _⊕_ f g = λ x → f x ⊕ g x

notogawa

-- 各データ型に対する帰納法の定義を考えると，
-- ≡の定義の仕方(parameter1つとindex1つ/index2つ)による差がわかる
module Ind where

-- ℕ
data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

-- ℕに関する帰納法

notogawa

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
import Prelude hiding ( (+) )
import qualified Prelude as P

class FuzzyAddable a b c where
    (+) :: a -> b -> c
instance FuzzyAddable String Int String where
    a + b = a ++ show b
instance Num a => FuzzyAddable a a a where