小编Quy*_*yen的帖子

我真的不了解函数(parse_list)

None -> List.rev is 和 None -> []

let try_parse parse x = try Some (parse x) with Error _ -> None;;

let parse_list parse =
  let rec aux is = function
    | [] -> List.rev is, []
    | (hd :: tl) as xs ->
    match try_parse parse hd with
      | Some i -> aux (i::is) tl
      | None -> List.rev is, xs
  in aux [];;

和

let parse_list parse =
  let rec aux is = function …

我有这种类型

Inductive coef :=
| Mycoef_ex2 : matrix -> coef
with matrix :=
| My_matrix : list (list coef) -> matrix.

Inductive my_type :=
| Mytype_ex1 : list my_type  -> my_type
| Mytype_int : Z -> my_type
| Mytype_coef : coef -> my_type.

在Ocaml我可以这样写:

let test_mytype := function
| Mytype_ex1 [Mytype_coef (Mycoef_ex2 (My_matrix m)); Mytype_int i] :: ps -> ...

我想使用参数m并i在同一函数中,我的函数需要两个参数.但是Coq我不能这样做,例如,如果我写入Coq

Definition test_mytype (m: my_type) :=
 match m with
  | Mytype_ex1 …

这是一个函数,我计算出一个等价类是一组完全等价的元素.而是迭代迭代矩阵列中的所有条目; 计算具有关系反射性的等价类并检查两个方向

let eq_class m i =
  let column = m.(i)
  and set = ref [] in
  Array.iteri begin fun j l ->
    if j = i || column.(j) && m.(j).(i) then
      set := j :: !set else ignore l
  end column;
  !set;;

你可以帮我解释一下l,我必须用来ignore传递编译器.如何在l不使用的情况下正确编写此功能ignore？

我在int进入Ocaml的转换类型int32.我更改了StringOcaml库的一些功能(下面的代码)

external length : string -> int32 = "%string_length"
external create: int32 -> string = "caml_create_string"
external unsafe_blit : string -> int32 -> string -> int32 -> int32 -> unit
  = "caml_blit_string" "noalloc"

let sub s ofs len =
  if ofs < 0l or len < 0l or add ofs len > length s
  then invalid_arg "String.sub"
  else begin
    let r = create len in
    unsafe_blit s ofs r 0l len;
    r
  end

请注意,我在 …