11.1. 强制插入
搜索从一种类型到另一种类型的强制转换的过程称为 coercion insert。 在以下可能会发生错误的情况下会尝试强制插入：
-
术语的预期类型与为该术语找到的类型不同。
-
需要类型或命题，但该术语的类型不是 universe。
-
术语的应用就像函数一样，但其类型不是函数类型。
当明确请求时，也会插入强制转换。 可以插入强制转换的每种情况都有一个相应的前缀运算符来触发适当的插入。
由于强制转换是自动插入的，因此嵌套的 type ascriptions 提供了一种精确控制强制转换中涉及的类型的方法。
如果 α 和 β 不是同一类型，((e : α) : β) 会将 e 安排为类型 α，然后插入从 α 到 β 的强制转换。
当发现强制转换时，用于查找它的实例将展开并从结果项中删除。
在可能的情况下，最终术语中不会发生对 Coe.coe 和相关函数的调用。
这个展开过程使术语更具可读性。
更重要的是，这意味着强制可以通过将强制项包装在函数中来控制对强制项的求值。
Controlling Evaluation with Coercions
结构 Later 表示将来可以通过调用所包含的函数来计算的项。
structure Later (α : Type u) where
get : Unit → α
从任何值到后面的值的强制转换是通过创建一个包装它的函数来执行的。
instance : CoeTail α (Later α) where
coe x := { get := fun () => x }
但是，如果强制插入导致应用 CoeTail.coe，则此强制在运行时不会产生预期效果，因为将评估强制值，然后将其保存在函数的闭包中。
由于强制实现已展开，因此该实例仍然有用。
def tomorrow : Later String :=
(Nat.fold 10000
(init := "")
(fun _ _ s => s ++ "tomorrow") : String)
打印结果定义表明计算是在函数体内进行的：
#print tomorrow
Duplicate Evaluation in Coercions
由于 Coe 实例的内容在强制插入期间展开，因此多次使用其参数的强制应小心确保计算仅发生一次。
这可以通过使用不属于实例的辅助函数来完成，或者使用 Lean.Parser.Term.let : term`let` is used to declare a local definition. Example:
```
let x := 1
let y := x + 1
x + y
```
Since functions are first class citizens in Lean, you can use `let` to declare
local functions too.
```
let double := fun x => 2*x
double (double 3)
```
For recursive definitions, you should use `let rec`.
You can also perform pattern matching using `let`. For example,
assume `p` has type `Nat × Nat`, then you can write
```
let (x, y) := p
x + y
```
The *anaphoric let* `let := v` defines a variable called `this`.
let 来评估强制项，然后重用其结果值。
结构 Twice 要求两个字段具有相同的值：
structure Twice (α : Type u) where
first : α
second : α
first_eq_second : first = second
定义从 α 到 Twice α 的强制转换的一种方法是使用辅助函数 twice。
coe 属性将其标记为强制，以便可以在证明目标和错误消息中正确显示。
@[coe]
def twice (x : α) : Twice α where
first := x
second := x
first_eq_second := rfl
instance : Coe α (Twice α) := ⟨twice⟩
当 Coe 实例展开时，对 twice 的调用仍然存在，这会导致在执行函数体之前计算其参数。
因此，Lean.Parser.Term.dbgTrace : term`dbg_trace e; body` evaluates to `body` and prints `e` (which can be an
interpolated string literal) to stderr. It should only be used for debugging.
dbg_trace 仅包含在结果项中一次：
#eval ((dbg_trace "hello"; 5 : Nat) : Twice Nat)
这是用来演示效果的：
将帮助程序内联到 Coe 实例中会产生与 Lean.Parser.Term.dbgTrace : term`dbg_trace e; body` evaluates to `body` and prints `e` (which can be an
interpolated string literal) to stderr. It should only be used for debugging.
dbg_trace 重复的术语：
instance : Coe α (Twice α) where
coe x := ⟨x, x, rfl⟩
#eval ((dbg_trace "hello"; 5 : Nat) : Twice Nat)
为评估结果引入中间名称可防止 Lean.Parser.Term.dbgTrace : term`dbg_trace e; body` evaluates to `body` and prints `e` (which can be an
interpolated string literal) to stderr. It should only be used for debugging.
dbg_trace 的重复：
instance : Coe α (Twice α) where
coe x := let y := x; ⟨y, y, rfl⟩
#eval ((dbg_trace "hello"; 5 : Nat) : Twice Nat)