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

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，如果省略的部分是一个表达式，它甚至在句法上是有效的，就像这里一样。因此，如果您正在编写精益练习，并且希望提供 reader 可以尝试填写的部分填写的答案：

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

它与_的不同之处在于，当您使用sorry时，精益不会尝试填空。

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

How to leave out a part of programming code, in a programming code quote?

quotes

lean