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.

ayu-mushi

{-# Language GADTs #-}
module Main where
import Control.Monad.Cont

data Proper = John | Mary -- Proper -> john | mary
data Det = A | The -- DET -> a | the
data N = Man | Woman -- N -> man | woman
data NP = NP0 Det N | NP1 Proper -- NP -> Det N | Proper
data VI = Sleeps | Walks -- VI -> sleeps | walks
data VT = Loves -- VT -> loves

ayu-mushi

function makeZako(n){
    return {hp: 20, mp:20, name:"zako" + n};
}

var enemies = [makeZako(0), makeZako(1), makeZako(2), makeZako(3)];

var player = {hp: 20, mp:20, name:"yuusya"};