小编Mus*_*oli的帖子

我是 Coq 的新手，想知道以下内容之间有什么区别：

Class test (f g: nat -> nat) := {
  init:   f 0 = 0 /\ g 0 = 0;
  output: ...another proposition about f and g...;
}.

和

Class test := {
  f: nat -> nat;
  g: nat -> nat;
  init:   f 0 = 0 /\ g 0 = 0;
  output: ...another proposition about f and g...;
}.

有人能提供解释吗？