Skip to content

Instantly share code, notes, and snippets.

View ayu-mushi's full-sized avatar
💛

ayu-mushi ayu-mushi

💛
View GitHub Profile
@ayu-mushi
ayu-mushi / population-processing.hs
Created November 14, 2019 14:36
population-processing
{-# LANGUAGE TupleSections #-}
module Lib
( someFunc
) where
import Text.Parsec
import System.IO
import Data.List
import Graphics.Gnuplot.Simple
import Control.Monad.Reader
@ayu-mushi
ayu-mushi / issei_attack.js
Created September 9, 2019 07:59
issei_attack
function Maou(){
this.hp = 100;
this.name = "魔王";
}
Maou.prototype.attack = function(aite) {
// 魔王の攻撃
alert(aite + "に魔王が二重攻撃!!");
};
function Cribou(){
@ayu-mushi
ayu-mushi / rpg.js
Created September 9, 2019 07:55
rpg.js
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"};
{-# 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
ayu-mushi / coq7.v
Last active June 7, 2019 14:36
Coq 練習問題(7)
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
ayu-mushi / coq6.v
Last active June 4, 2019 10:51
Coq exercise (6)
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
ayu-mushi / coq5.v
Created May 22, 2019 01:50
Coq練習問題(5)
a
@ayu-mushi
ayu-mushi / coq4.v
Last active May 15, 2019 08:47
coq練習問題(4)
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
ayu-mushi / coq3.v
Last active May 12, 2019 06:35
coq練習問題(3)
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
ayu-mushi / coq2.v
Last active April 30, 2019 11:45
Coq練習問題(2)
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.