如何在编程代码报价中删除编程代码的一部分

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具有 sorry，如果省略的部分是一个表达式，它甚至是语法上的valid，因为它在这里。因此，如果您要写一个练习，并且想要提供一个部分填充的答案，读者可以尝试填写：

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

它与_不同，当您使用sorry时，精益不会尝试填充空白。