小编Fab*_*cke的帖子

我有一个查询,我必须从DB2数据库中排序结果.查询将选择列empname,salary,status.但我必须使用empno按顺序对结果进行排序
但查询不起作用..这是查询.

select empname, salary, status from emp where salary>5000 order by empno  

您是否可以更新查询以排序empno而不使用它来选择列？

我偶然发现了OCaml中的以下编译消息:

This simple coercion was not fully general. Consider using a double coercion.

它发生在相当复杂的源代码中,但这是一个MNWE:

open Eliom_content.Html.D

let f_link s =
  let arg : Html_types.phrasing_without_interactive elt list = [pcdata "test"] in
  [ Raw.a ~a:[a_href (uri_of_string (fun () -> "test.com"))] arg ]

type tfull = (string -> Html_types.flow5 elt list)
type tphrasing = (string -> Html_types.phrasing elt list)

let a : tfull = ((f_link :> tphrasing) :> tfull)

let b : tfull = (f_link :> tfull)

您可以在ocamlfind ocamlc -c -package eliom.server …

我正在使用在线书籍“软件基础”来了解 Coq。

第二章要求证明“plus_assoc”定理：

Theorem plus_assoc : forall n m p : nat, n + (m + p) = (n + m) + p.

我利用了两个先前证明的定理：

Theorem plus_comm : forall n m : nat, n + m = m + n.
Theorem plus_n_Sm : forall n m : nat, S (n + m) = n + (S m).

我在 n 上使用归纳证明了 plus_assoc 定理：

Proof.
  intros n m p.
  induction n as [ | n' ].
    reflexivity.

    rewrite plus_comm.
    rewrite <- plus_n_Sm.
    rewrite …