ayu-mushi

import Control.Monad
import Control.Applicative


-- filterM (const [True, False])

-- filterM :: (Applicative m) => (a -> m Bool) -> [a] -> m [a]
-- filterM p = foldr (\x -> liftA2 (\flg -> if flg then (x:) else id) (p x)) (pure [])

-- (<*>) :: [a -> b] -> [a] -> [b]

ayu-mushi

MAILTO="[email protected]"
SHELL=/bin/zsh
PATH=/usr/local/lib/anaconda2/bin/:/opt/mozart/bin/:/usr/local/ghc-7.10/bin:/usr/local/ghc-7.8.4/bin:/usr/local/ghc-7.10.2/bin/:/usr/local/bin:~/.local/bin:/opt/local/bin:/usr/local/ghc-7.8/bin:~/.cabal/bin/:/sbin:/bin:/usr/sbin:/usr/bin:/usr/local/bin/

HOME=/home/ayu-mushi
LANG=ja_JP.UTF-8
LC_ALL=ja_JP.UTF-8
CONTENT_TYPE=text/plain; charset=UTF-8

ayu-mushi

var request = require('request');

url = 'https://query.wikidata.org/sparql'

var query="SELECT\
  ?countriesLabel ?countriesDescription ?capitalLabel ?capitalDescription ?inception ?abolished ?dummy\
WHERE {\
  {?countries rdfs:label \"" + process.argv[2] +
  "\"@ja; wdt:P31 wd:Q3624078}\
  UNION {?countries skos:altLabel \"" + process.argv[2] +

ayu-mushi

Require Import ssreflect.
Section Coq1.
  Variable P Q R : Prop.
  Theorem imp_trans : (P -> Q) -> (Q -> R) -> P -> R.
  Proof.
    intros p q r.
    apply q.
    apply p.
    assumption.
  Qed.

ayu-mushi

Require Import ssreflect.
Section Coq3.
  Variable A : Set.
  Variable R : A -> A -> Prop.
  Variable P Q : A -> Prop.

  Theorem exists_postpone : (exists x, forall y, R x y) -> (forall y, exists x, R x y).
  Proof.
    move => [ea] y.
    move => y0.

ayu-mushi

Require Import ssreflect.

Lemma plusnS m n : m + S n = S (m + n).
Proof.
  elim: m => /=.
  + done.
  + move => m IH.
    by rewrite IH.
Qed.
Lemma plusSn m n : (S m) + n = S (m + n).

ayu-mushi

Require Import ssreflect.

Module Odd.

Inductive odd : nat -> Prop :=
  | odd_1 : odd 1
  | odd_SS : forall n, odd n -> odd (S (S n)).
Inductive even : nat -> Prop :=
  | even_0 : even 0
  | even_SS : forall n, even n -> even (S (S n)).

ayu-mushi

a

ayu-mushi

Require Import ssreflect.
From mathcomp Require Import all_ssreflect.
Require Import Extraction.


Section Sort.
Variables (A:Set) (le:A->A->bool).

(* 既に整列されたリストlの中にaを挿入する *)
Fixpoint insert a (l: list A) := match l with

ayu-mushi

Require Import ssreflect.
From mathcomp Require Import all_ssreflect.
Require Import Extraction.


(* 練習問題5.1 *)

Section sort.
Variable A : eqType.
Variable le : A -> A -> bool.