erutuf

intFib :: [Int]
intFib = 1:1:zipWith (+) intFib (tail intFib)

fib :: [Integer]
fib = map fromIntegral intFib

main = print $ fib !! 1000000

erutuf

[    28.938] 
X.Org X Server 1.9.0
Release Date: 2010-08-20
[    28.938] X Protocol Version 11, Revision 0
[    28.938] Build Operating System: Linux 2.6.24-27-server i686 Ubuntu
[    28.939] Current Operating System: Linux mirai-laptop 2.6.31-14-generic #48-Ubuntu SMP Fri Oct 16 14:04:26 UTC 2009 i686
[    28.939] Kernel command line: BOOT_IMAGE=/boot/vmlinuz-2.6.31-14-generic root=UUID=57911c9a-b82b-4431-ba6d-653522ae3186 ro quiet splash
[    28.939] Build Date: 16 September 2010  05:39:22PM
[    28.939] xorg-server 2:1.9.0-0ubuntu7 (For technical support please see http://www.ubuntu.com/support) 
[    28.939] Current version of pixman: 0.18.4

erutuf

#
# Catch-all evdev loader for udev-based systems
# We don't simply match on any device since that also adds accelerometers
# and other devices that we don't really want to use. The list below
# matches everything but joysticks.

Section "InputClass"
        Identifier "evdev pointer catchall"
        MatchIsPointer "on"
        MatchDevicePath "/dev/input/event*"

erutuf

module Neko where

data どうぶつ : Set where
    ねこ : どうぶつ
    その他 : どうぶつ 

data なきごえ : Set where
    にゃー : なきごえ
    あばば : なきごえ

erutuf

module Msort2 where

open import Level renaming (zero to lzero)
open import Data.Bool
open import Data.Nat renaming (ℕ to nat)
open import Data.List renaming (_∷_ to _::_)
open import Relation.Binary using (Rel)
open import Induction.WellFounded as WF
open import Induction.Nat

erutuf

\documentclass{jarticle}

%\usepackage[dvips]{graphicx}

\setlength{\textwidth}{150mm}
\setlength{\textheight}{232mm}

\setlength{\oddsidemargin}{5mm}
\setlength{\topmargin}{5mm}

erutuf

{-# OPTIONS --universe-polymorphism #-}

module Order where

data Level : Set where
  zero : Level
  suc  : (i : Level) → Level

{-# BUILTIN LEVEL     Level #-}

erutuf

{-# OPTIONS --universe-polymorphism #-}

module Msort where

open import Level
open import Data.Nat
open import Data.Sum 
open import Data.Unit
open import Data.Empty

erutuf

module HaityuuOishii where

data False : Set where

data _\/_ (P Q : Set) : Set where
    orl : P -> P \/ Q
    orr : Q -> P \/ Q

haityu : (P : Set) -> (forall (P : Set) -> ((P -> False) -> False) -> P) -> (P \/ (P -> False))
haityu P nnp = nnp (P \/ (P -> False)) (\ z -> z ((orr (\ x -> z (orl x)))))

erutuf

module Joshiryoku where

infix 1 >_< ^_^ ・_・
infix 2 （_） [_]
infix 3 o_o ∩_∩

data Mouse : Set where
    O : Mouse
    - : Mouse
    ω : Mouse