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 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 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

// 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

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

;;; -*- mode: emacs-lisp; coding: utf-8-unix; indent-tabs-mode: nil -*-

(when (require 'haskell-mode nil t)
  (when (require 'haskell-cabal nil t)
    (autoload 'offside-trap-mode "mode/haskell/offside-trap/offside-trap.el")

    (add-to-list 'auto-mode-alist '("\\.[hg]s$" . haskell-mode))
    (add-to-list 'auto-mode-alist '("\\.hi$" . haskell-mode))
    (add-to-list 'auto-mode-alist '("\\.l[hg]s$" . literate-haskell-mode))
    (add-to-list 'auto-mode-alist '("\\.cabal\\'" . haskell-cabal-mode))

notogawa

#define Q(c)*q=#c;c
Q(main(n){for(scanf("%d",&n);n--;)printf("#define Q(c)*q=#c;c\nQ(%s)",q);})

notogawa

-- http://people.inf.elte.hu/divip/AgdaTutorial/Functions.Equality_Proofs.html
module Theorem where

import Level

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

{-# BUILTIN NATURAL ℕ    #-}

notogawa

-- AをaにBをbにeps近似で，めんどうなので 0 < a, 0 < b に限定するけど
innerQ :: Rational -> Rational -> Rational
innerQ a b | a > b = innerQ b a
innerQ a b = head $ [1 .. d 1] >>= f 1 where
    -- マジメにやるなら2分探索とか
    d n | 1 / n < b - a = n | otherwise = d (n+1)
    f n x | b < n / x = []
          | a < n / x && n / x < b = [n / x] -- 近似時のeps分も入れれば確実にAとBの間に入る
          | n / x < a = f (n+1) x

notogawa

{-# LANGUAGE GADTs #-}
{-# LANGUAGE FunctionalDependencies #-}

-- 0/1/二項演算op2 だけしか無い式の構文で，
-- 0が高々1回しか表れないようなものを表現し，
-- Eqのインスタンスにしたい．

class ContainsZeroAtMostOne a where

data WithZero