erutuf

Require Import List.

Open Scope list_scope.

Import ListNotations.

Variable String : Type.

Axiom string_eq_dec : forall s1 s2 : String, {s1 = s2} + {s1 <> s2}.

erutuf

Require Import Arith.
Require Import List.

Open Scope list_scope.

Import ListNotations.

Variable String : Type.

Axiom string_eq_dec : forall s1 s2 : String, {s1 = s2} + {s1 <> s2}.

erutuf

Require Import ssreflect.

Lemma exo5 : forall A B C : Prop, A /\ B <-> B /\ A.
Proof.
move=> A B P.
split.
  case.
  move=> a b.
  split.
    exact b.

erutuf

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

fib :: [Integer]
fib = map fromIntegral intFib

main = print $ fib !! 1000000

erutuf

Require Import List.

Variable A B : Type.

Theorem fold_symmetric2 : forall (f : A -> B -> A) (g : B -> A -> A),
  (forall x y, f x y = g y x) ->
  forall x l, fold_left f l x = fold_right g x (rev l).
Proof with simpl in *; intuition.
intros f g H x l. revert x.
induction l...

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}