让 Kubic 来吧！

dottle · 2024-03-05 00:10:12 · 闲话

我们特此认可并明确 Coq 语言需要中文翻译，这是为了或许能赢得中国成为最强国的战役。

这是一段原文：

Theorem mult_plus_distr_r : forall n m p : nat,
  (n + m) * p = (n * p) + (m * p).
Proof.
  intros n m p.
  induction n as [| n' N].
    - reflexivity.
    - simpl. 
      rewrite N. 
      rewrite add_assoc. 
      reflexivity.
Qed.

翻译之后如下：

我们特此声明并确认 mult_plus_distr_r : 对所有的 n m p : nat,
    (n + m) * p = (n * p) + (m * p).
让我来吧.
   让 n m p 来吧.
   继而 n 不断作为 [| n' N] 自我延申.
      - 比特是万物；万物是比特。
      - 尽情探索享受.
        我们特此明确 N.
        我们特此明确 add_assoc.
        比特是万物；万物是比特。
欢歌载舞，交换比特，共同庆祝.