Coq |
Ocaml |
Coq < Check 3.
3
: nat
|
# 3;;
- : int = 3
|
Coq < Require Import String.
Coq < Open Scope string_scope.
Coq < Check "Hello world".
"Hello world"
: string
|
# "Hello world";;
- : string = "Hello world"
|
Coq < Require Import Ascii.
Coq < Open Scope char_scope.
Coq < Check "J".
"J"
: ascii
|
# 'J';;
- : char = 'J'
|
Coq < Check true.
true
: bool
|
# true;;
- : bool = true
|
Coq < Check tt.
tt
: unit
|
# ();;
- : unit = ()
|
Coq < Check (3, true, "hi").
(3%nat, true, "hi")
: nat * bool * string
|
# (3,true,"hi");;
- : int * bool * string = 3, true, "hi"
|
Coq < Require Import List.
Coq < Check 1::2::3::nil.
1 :: 2 :: 3 :: nil
: list nat
|
# [1;2;3];;
- : int list = [1; 2; 3]
|
ない
|
# [|1;2;3|];;
- : int array = [|1; 2; 3|]
|
Coq |
Ocaml |
Variable A:Set.
Definition get_opt (opt:option A) d :=
match opt
with
None =>
d
| Some x
=> x
end.
|
let get_opt (opt, d) =
match opt
with
None -> d
| Some x
-> x
|
Require Import List.
Fixpoint take n xs {struct n} :=
xs<>nil ->
match n, xs
with
O, xs => nil
| S m, (x::xs)
=> x :: take m xs
  end.
|
let rec take n xs
=
match n, xs
with
0, xs -> []
| n, []
-> failwith "take"
| n, x::xs
-> x :: take (n-1) xs
|
Coq |
Ocaml |
Require Import ZArith.
Require Import QArith.
Require Import string.
Open Scope type_scope.
Definition foo := Z * Q * string
|
type foo =
int * float *
string
|
Definition bar :=
(0%Z, (314#100)%Q, "hi"%string)
|
let bar =
0, 3.14, "hi"
or
let bar =
(0, 3.14, "hi")
|
Check(snd (fst bar))
|
match bar
with
_,x,_
-> x
or
let
_,x,_
= bar
in x
|