fetburner

(* ソフトウェアの基礎より *)
Require Import List Arith.

Notation "[ ]" := nil.
Notation "[ x , .. , y ]" := (cons x .. (cons y []) ..).
Notation "x ++ y" := (app x y) 
                     (at level 60, right associativity).

(* 変数の識別子 *)
Inductive id : Type :=

fetburner

#load "graphics.cma";;
let ( @. ) f g x = f (g x)

let rec natural acc = function
  | 0 -> acc
  | n -> natural (n :: acc) (n - 1)
let natural = natural []

let complex_of_pos (x, y) =
  (-1.5 +. float_of_int x *. 2. /. float_of_int (Graphics.size_x ()),

fetburner

(** val fold_left : ('a1 -> 'a2 -> 'a1) -> 'a2 list -> 'a1 -> 'a1 **)

fun fold_left f l a0 =
  case l of
    [] => a0
  | b::t => fold_left f t (f a0 b)

(** val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1 **)

fun fold_right f a0 l =

fetburner

x = wavread("./WonChuKissMe.wav");
N = 255;
n = 0:N - 1;
subplot(2, 1, 1);
plot(n, x(1:N)); grid;
title('Input signal x(n)'); xlabel('time n'); ylabel('x(n)');
h = [0.0464, 0.1522, 0.2037, 0.2536, 0.2037, 0.1522, 0.0464];
y = filter(h, 1, x);
subplot(2, 1, 2);
plot(n, y(1 : N)); grid;

fetburner

let trick = ['T'; 'r'; 'i'; 'c'; 'k']
let n = List.length trick

let title =
  [("桜色のはじまり", "やきそばとベランダと女の子");
  ("もうひとつの桜色", "放課後はハリーちゃんと♥");
  ("会長はお姉ちゃん", "プール掃除でお約束");
  ("すっぱい大作戦?", "もしかして肝試し!?");
  ("お姉ちゃんとお茶しよう!", "魔女とリンゴとお姉ちゃんと");
  ("文化祭だよ☆お泊まりです♥", "文化祭だよ☆本番です!");

fetburner

The following actions will be performed:
 - install lacaml.7.1.3 [required by slap]
 - downgrade ocp-build.1.99.8-beta to 1.99.6-beta
 - install slap.0.0.0
 - recompile ocp-indent.1.4.2 [use ocp-build]
2 to install | 1 to reinstall | 0 to upgrade | 1 to downgrade | 0 to remove
Do you want to continue ? [Y/n] y

=-=-= Removing Packages =-=-=
Removing ocp-indent.1.4.2.

fetburner

Section QSort.
Require Import Arith List Program Bool Recdef.

Variable A : Type.
Variable compare : A -> A -> comparison.

Definition partition (p : A -> bool) l :=
  fold_left (fun (acc : list A * list A) x =>
    let (ltrue, lfalse) := acc in
    if p x then (x :: ltrue, lfalse)

fetburner

(* 添字も渡すmap *)
fun mapi f =
  rev
    o #1
    o foldl (fn (x, (result, i)) => (f (i, x) :: result, i + 1)) ([], 0)

(* 回数の上限に達するか終了条件を満たすまで計算を反復する *)
fun iterateWhile fin f =
  let 
    fun iterateWhileAux acc 0 x = acc

fetburner

(** val app : 'a1 list -> 'a1 list -> 'a1 list **)

val app = (fn x => fn y => x @ y)

signature TotalLeBool' = 
 sig 
  type t 
  
  val leb : t -> t -> bool
 end

fetburner

Require Import Arith Relations FunctionalExtensionality.

(* 変数の識別子 *)
Definition id := nat.

(* 状態 *)
Definition state := id -> nat.

Definition beq_id : id -> id -> bool := beq_nat.
Definition X := 0.