ayu-mushi

From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.

Lemma eq (p q r : Prop): (p <-> q) -> ((p -> r) <-> (q -> r)).
Proof.
  move => [pq qp].
  split.
  move => pr q0.
  apply pr.
  apply qp.

ayu-mushi

{-# 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

module Main exposing (main)

import Browser
import Browser.Events exposing (onAnimationFrameDelta)
import Canvas exposing (rect, shapes)
import Canvas.Settings exposing (fill)
import Canvas.Settings.Advanced exposing (rotate, transform, translate)
import Color
import Html exposing (Html, div)
import Html.Attributes exposing (style)

ayu-mushi

function Maou(){
	this.hp = 100;
    this.name = "魔王";
}
Maou.prototype.attack = function(aite) {
  // 魔王の攻撃
  alert(aite + "に魔王が二重攻撃！！");
};

function Cribou(){

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"};

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

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

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

a

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)).