quotes - 如何在编程代码引用中省略一部分编程代码？

Question

如何在编程代码引用中省略一部分编程代码？

特别是我有以下代码片段（来自精益证明助手）：

def single (a : α) (b : β) : α →₀ β :=
⟨λa', if a = a' then b else 0,
  finite_subset (@finite_singleton α a) $ assume a', by by_cases h : a = a'; 
  simp [h]⟩

我想省略一部分，比如：

def single (a : α) (b : β) : α →₀ β :=
⟨λa', if a = a' then b else 0,
  [...]⟩

对于文本引用，我知道我们可以使用 [...] 来省略部分引用。

但是在编程代码引号的情况下我们使用什么？

Answer 1

Lean has sorry，如果省略的部分是一个表达式，它甚至在语法上是有效的，就像这里一样。因此，如果您正在编写一个精益练习，并且您想提供一个部分填写的答案，读者可以尝试填写：

def single (a : α) (b : β) : α →₀ β :=
⟨λa', if a = a' then b else 0,
  sorry⟩

不同之处_在于，Lean 不会在你使用sorry.