This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE TupleSections #-} | |
module Lib | |
( someFunc | |
) where | |
import Text.Parsec | |
import System.IO | |
import Data.List | |
import Graphics.Gnuplot.Simple | |
import Control.Monad.Reader |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
function Maou(){ | |
this.hp = 100; | |
this.name = "魔王"; | |
} | |
Maou.prototype.attack = function(aite) { | |
// 魔王の攻撃 | |
alert(aite + "に魔王が二重攻撃!!"); | |
}; | |
function Cribou(){ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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"}; | |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Import ssreflect. | |
From mathcomp Require Import all_ssreflect. | |
Require Import Extraction. | |
(* 練習問題5.1 *) | |
Section sort. | |
Variable A : eqType. | |
Variable le : A -> A -> bool. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
a |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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)). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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. |