Option<T> Option<T> 是 Rust 里表示“可能有值、可能没有”的类型，只有两种取值： Some(x) Some(x) 和 None None 。在返回 Option Option 的函数里，表达式 e? e? 的意思是：

• 如果 e e 是 Some(x) Some(x) ，整个 e? e? 的值就是 x x ，继续往下执行；
• 如果 e e 是 None None ，函数立刻返回 None None ，后面的代码不再执行。

在 Rust 求值器 step step 中， Succ(t1) Succ(t1) 匹配一个后继项， step(t1) step(t1) 返回 Option<Term> Option<Term> ，表示子项是否存在一步后继。这个分支可以写成两种等价形式：

// 用 ?
Succ(t1) => Some(Succ(Box::new(step(t1)?))),

// 不用 ?，展开写
Succ(t1) => match step(t1) {
    Some(t1_) => Some(Succ(Box::new(t1_))),
    None => return None,
},

// 用 ?
Succ(t1) => Some(Succ(Box::new(step(t1)?))),

// 不用 ?，展开写
Succ(t1) => match step(t1) {
    Some(t1_) => Some(Succ(Box::new(t1_))),
    None => return None,
},

例如，读取字符串的首字符，并把 ASCII 小写字母转成大写：

fn first_char_upper(s: &str) -> Option<char> {
    let c = s.chars().next()?;   // 空字符串时这里直接返回 None
    Some(c.to_ascii_uppercase())
}
assert_eq!(first_char_upper("rust"), Some('R'));
assert_eq!(first_char_upper(""), None);

fn first_char_upper(s: &str) -> Option<char> {
    let c = s.chars().next()?;   // 空字符串时这里直接返回 None
    Some(c.to_ascii_uppercase())
}
assert_eq!(first_char_upper("rust"), Some('R'));
assert_eq!(first_char_upper(""), None);

对照 [定义] 一步归约 中的同余规则：E-Succ 说“若 ${𝑡}_1⟶{𝑡}_{1^{\prime }}$，则 $\text{succ }{𝑡}_1⟶\text{ succ }{𝑡}_{1^{\prime }}$”。 step(t1)? step(t1)? 先去找 ${𝑡}_{1^{\prime }}$，找到了就拿来搭结论；找不到（前提不成立），结论就推不出来，整个函数返回 None None 。这正好是“子项不能归约，整个项也不能沿这条规则归约”。 类型检查器 type_of type_of 里的 type_of(t1)? type_of(t1)? 也是同样的意思：按照 [定义] 类型与类型判断 的规则，子项没有类型，就无法满足相应构造的定型前提，检查器返回 None None 。