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

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

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