我发现下面两个表达式
#eval have amount : Nat := 5 ; amount*4以及
#eval let amount : Nat := 5 ; amount*4行为完全相同。证明定理时也是这样。 它们可以互换吗？区别在哪里？
I've observed that these two expressions
#eval have amount : Nat := 5 ; amount*4and
#eval let amount : Nat := 5 ; amount*4behave identically. This also happens in theorem proofs. Are they interchangeable? How do they differ?
have 的工作方式如下
在内部，have h : p := s; t 会成为项 (fun (h : p) => t) s。换句话说，s 证明 p，而 t 在假设 h : p 下证明所需结论，然后通过 lambda 抽象和应用把两者结合起来。
let 的工作方式如下
let 结构提供了更强的缩写方式，因此有些 let a := t1; t2 形式的表达式无法表示为 (fun a => t2) t1。可以练习思考一下，为什么下面的 keepType 定义能通过类型检查，而 loseType 不能。
def keepType := let chosen := Nat; fun item : chosen => item + 4
/-
def loseType := (fun chosen => fun item : chosen => item + 4) Nat
-/Here is how have operates
Internally, have h : p := s; t becomes the term (fun (h : p) => t) s. Put differently, s proves p, while t proves the intended conclusion under the assumption h : p, and lambda abstraction followed by application joins them together.
Here is how let operates
The let construct provides more powerful abbreviation, so some expressions let a := t1; t2 have no equivalent (fun a => t2) t1. For practice, work out why the definition called keepType below passes type checking while loseType does not.
def keepType := let chosen := Nat; fun item : chosen => item + 4
/-
def loseType := (fun chosen => fun item : chosen => item + 4) Nat
-/区别在于 let 保留定义，而 have 会丢弃它。
例如，在 Lean 4 中，下面的例子使用 let 可以通过，但换成 have 就会失败。
example : {item : Nat // item = 0} := let item := 0 ; ⟨item, rfl⟩通常，证明使用 have，其他情况使用 let。在 Lean3 的策略模式中，可以用 dsimp [x] 展开 let x := ... 的定义，但我不知道 Lean4 中对应的做法。
The distinction is that let retains a definition, whereas have discards it.
For instance, this example accepts let, but substituting have fails in Lean 4.
example : {item : Nat // item = 0} := let item := 0 ; ⟨item, rfl⟩Typically, proofs use have, while other things use let. Within Lean3's tactic mode, dsimp [x] lets you unfold let x := ..., but I don't know the corresponding approach in Lean4.
看一个更实用的例子:
def divisibleByTwo (number : Nat) : Prop :=
∃ factor : Nat, number = factor * 2
theorem doubled_half (number : Nat) : divisibleByTwo (number / 2 * 2) :=
let half := number / 2
have : number / 2 * 2 = half * 2 := rfl
Exists.intro half this
theorem doubled_failure (number : Nat) : divisibleByTwo (number / 2 * 2) :=
have half := number / 2
have : number / 2 * 2 = half * 2 := rfl -- error: type mismatch
Exists.intro half this第一个证明可以通过，而第二个在 rfl 表达式处失败。这是因为 let 把后续出现的所有 half 都替换为定义 number / 2。然而，使用 have 后，编译器只保留 half 的类型是 Nat 这一信息，并丢弃其定义，因此 rfl 无法把 number / 2 * 2 与任意的 half / 2 等同起来。
所以我们通常用 have 引入中间命题或引理，因为类型系统只需要知道某个命题有证明，并不关心实际的证明过程。相反，当后面的证明需要变量的定义时，我们会用 let 引入变量。
Consider this example with a practical use:
def divisibleByTwo (number : Nat) : Prop :=
∃ factor : Nat, number = factor * 2
theorem doubled_half (number : Nat) : divisibleByTwo (number / 2 * 2) :=
let half := number / 2
have : number / 2 * 2 = half * 2 := rfl
Exists.intro half this
theorem doubled_failure (number : Nat) : divisibleByTwo (number / 2 * 2) :=
have half := number / 2
have : number / 2 * 2 = half * 2 := rfl -- error: type mismatch
Exists.intro half thisThe initial proof works, whereas the other one fails at its rfl expression. The reason is that let substitutes the definition number / 2 for all later uses of half. After have, however, the compiler retains only that half has type Nat and discards its definition, leaving rfl unable to identify number / 2 * 2 with an arbitrary half / 2.
Consequently, we normally introduce intermediate propositions or lemmas with have, since the type system needs evidence for the particular proposition without needing the proof's actual procedure. By contrast, let introduces variables when later parts of the proof need their definitions.
你好， 在一个我无法修改代码的包里，类的层次结构如下。 我想给 Inner 加个方便使用的包装，但因为 Inner 依赖外层实例，目前只做到把它放进外层类的子类里面。 可惜，在多个地方继承 Outer，就意味着每个新子类里都得重复这个方便使用的 ca…
我在创建一个 Map，其中每个条目都保存字符串数组。怎样在一条语句中同时声明类型并完成初始化？ 我（天真地）这样试了一下。 结果是下面这个错误。
为什么 Typescript 接受我的函数定义，虽然它与接口签名不同，但当我实际调用同一个函数时却报告问题。
