1
2
3
4
5
6
7
8
9
(** 普通のフィボナッチ関数の定義 *)
Fixpoint fib (n: nat) : nat :=
  match n with
    | 0 => 1
    | 1 => 1
    | S (S m as sm) => fib sm + fib m
  end.
 
(** CPS変換されたフィボナッチ関数の定義 *)
 ...

1
2
3
4
5
6
7
8
9
(* x番目のフィボナッチ が y となることを Fib x y と書き、以下で定義する *)
Inductive Fib : nat -> nat -> Prop :=
| Fib0: Fib 0 1
| Fib1: Fib 1 1
| FibSSn: forall n x y, Fib (S n) x -> Fib n y ->
  Fib (S (S n)) (x + y).
 
(* 関数fがフィボナッチの実装であるとは *)
Definition FibFunc (f: nat -> nat) := forall n, Fib n (f n).
 ...

1
2
3
4
5
6
7
8
9
let scan_int () = Scanf.scanf " %d" (fun x -> x);;
 
 
let rec liste_id=function(0,a::liste)->a
|(n,a::liste)->liste_id(n-1,liste);;
 
let rec enlever=function(0,liste)->liste
|(n,[])->[]
|(n,a::b)->enlever(n-1,b);;
 ...

1
2
3
4
5
6
7
8
9
let scan_int () = Scanf.scanf " %d" (fun x -> x);;
 
 
let rec liste_id=function(0,a::liste)->a
|(n,a::liste)->liste_id(n-1,liste);;
 
let rec enlever=function(0,liste)->liste
|(n,[])->[]
|(n,a::b)->enlever(n-1,b);;
 ...

1
2
3
4
5
6
7
8
9
let scan_int () = Scanf.scanf " %d" (fun x -> x);;
 
 
let rec liste_id=function(0,a::liste)->a
|(n,a::liste)->liste_id(n-1,liste);;
 
let rec enlever=function(0,liste)->liste
|(n,[])->[]
|(n,a::b)->enlever(n-1,b);;
 ...

1
2
3
4
5
6
7
8
9
let scan_int () = Scanf.scanf " %d" (fun x -> x);;
 
 
let rec liste_id=function(0,a::liste)->a
|(n,a::liste)->liste_id(n-1,liste);;
 
let rec enlever=function(0,liste)->liste
|(n,[])->[]
|(n,a::b)->enlever(n-1,b);;
 ...

1
2
3
4
5
6
7
8
9
let scan_int () = Scanf.scanf " %d" (fun x -> x);;
 
 
let rec liste_id=function(0,a::liste)->a
|(n,a::liste)->liste_id(n-1,liste);;
 
let rec enlever=function(0,liste)->liste
|(n,[])->[]
|(n,a::b)->enlever(n-1,b);;
 ...

1
2
3
4
5
6
7
8
9
let scan_int () = Scanf.scanf " %d" (fun x -> x);;
 
 
let rec liste_id=function(0,a::liste)->a
|(n,a::liste)->liste_id(n-1,liste);;
 
let rec enlever=function(0,liste)->liste
|(n,[])->[]
|(n,a::b)->enlever(n-1,b);;
 ...

1
2
3
4
5
6
7
8
9
let scan_int () = Scanf.scanf " %d" (fun x -> x);;
 
 
let rec liste_id=function(0,a::liste)->a
|(n,a::liste)->liste_id(n-1,liste);;
 
let rec enlever=function(0,liste)->liste
|(n,[])->[]
|(n,a::b)->enlever(n-1,b);;
 ...

1
2
3
4
5
6
7
8
9
let scan_int () = Scanf.scanf " %d" (fun x -> x);;
 
 
let rec liste_id=function(0,[a]@liste)->a
|(n,[a]@liste)->liste_id(n-1,liste);;
 
let rec enlever=function(0,liste)->liste
|(n,[])->[]
|(n,a::b)->enlever(n-1,b);;
 ...

1
2
3
4
5
6
7
8
9
let scan_int () = Scanf.scanf " %d" (fun x -> x);;
 
 
let rec liste_id(0,[a]@liste)->a
|(n,[a]@liste)->liste_id(n-1,liste);;
 
let rec enlever(0,liste)->liste
|(n,[])->[]
|(n,a::b)->enlever(n-1,b);;
 ...

1
2
3
4
5
6
7
8
9
Require Import Arith.
Require Import Recdef.
 
(** 普通のフィボナッチ関数の定義 *)
Function fib (n: nat) {measure id n} : nat :=
  match n with
    | 0 => 1
    | 1 => 1
    | S (S m) => fib (S m) + fib m
 ...

1
2
3
4
5
6
7
8
9
uire Import Arith.
Require Import Recdef.
 
(** 普通のフィボナッチ関数の定義 *)
Function fib (n: nat) {measure id n} : nat :=
  match n with
    | 0 => 1
    | 1 => 1
    | S (S m) => fib (S m) + fib m
 ...

1
2
3
4
5
6
7
8
9
Require Import Arith.
Require Import Recdef.
 
(** 普通のフィボナッチ関数の定義 *)
Function fib (n: nat) {measure id n} : nat :=
  match n with
    | 0 => 1
    | 1 => 1
    | S (S m) => fib (S m) + fib m
 ...

1
2
3
4
5
6
7
8
let rec fib_cps n (cont:int -> unit) : unit =
  match n with
  | 0 -> cont 1
  | 1 -> cont 1
  | n ->
    fib_cps (n-1) (fun r1 ->
      fib_cps (n-2) (fun r2 ->
        cont (r1 + r2)))
 ...

1
2
3
4
5
6
7
8
let rec fib_cps n (cont:int -> unit) : unit =
  match n with
  | 0 -> cont 1
  | 1 -> cont 1
  | n ->
    fib_cps (n-1) (fun r1 ->
      fib_cps (n-2) (fun r2 ->
        cont (r1 + r2)))
 ...

1
2
3
4
5
6
7
8
let rec fib_cps n (cont:int -> 'a) : 'a =
  match n with
  | 0 -> cont 1
  | 1 -> cont 1
  | n ->
    fib_cps (n-1) (fun r1 ->
      fib_cps (n-2) (fun r2 ->
        cont (r1 + r2)))
 ...

1
2
3
4
5
6
7
8
let rec fib_cps n cont =
  match n with
  | 0 -> cont 1
  | 1 -> cont 1
  | n ->
    fib_cps (n-1) (fun r1 ->
      fib_cps (n-2) (fun r2 ->
        cont (r1 + r2)))
 ...

1
let x = 2

1
2
 
 print_int -9%5;;

1
Printf.printf "Hello\n";;

1
2
3
4
5
6
7
8
9
Require Import Arith.
 
Theorem not_forall_exists : ~ (
  forall (A : Type) (P : A -> A -> Prop),
    (forall b : A, exists a : A, P a b) -> (exists a : A, forall b : A, P a b)
  ).
Proof.
intro.
elim (H nat (fun a b => b < a)).
 ...

1
2
3
4
5
6
7
8
9
Theorem not_forall_exists : ~ (
  forall (A : Type) (P : A -> A -> Prop),
    (forall b : A, exists a : A, P a b) -> (exists a : A, forall b : A, P a b)
  ).
Proof.
intro.
elim (H nat (fun a b => b < a)).
 induction x.
  intro HH; apply (lt_n_O 3 (HH 3)).
 ...

1
2
let d f = f * 2;;
d 3;;

1
2
let f = f * 2;;
f 3;;

1
2
3
4
5
6
7
8
9
let yg x y z=moveto x y;
set_color black;
fill_circle x y z;
set_color white;
fill_rect x (y-z) (2*z) (2*z);
fill_circle x (y+z/2) (z/2);
set_color black;
fill_circle x (y-z/2) (z/2);
draw_circle x y z;
 ...

1
2
3
4
5
6
7
8
9
open Map
 
module StringMap = Map.Make (String)
 
let rec range i j exclude = 
        if i > j then [] 
        else if i=exclude 
                then (range (i+1) j exclude) 
                else i :: (range (i+1) j exclude)
 ...

1
¸„ħ}ßnïÚæ“‘½–ä´CB»GH¥÷tf…VlÕÄe¢±Îü¨

1
2
3
4
5
let f ~foo = foo + foo
 
(* let _ = print_int (f ~foo:5) と同じ *)
let foo = 5
let _ = print_int (f ~foo)

1
2
3
4
5
let f ~foo = foo + foo
 
let _ = print_int (f ~foo:5)
let foo = 5
let _ = print_int (f ~foo)