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

In particular I have the following code snippet (from the Lean proof assistant):

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]⟩

And I want to leave out a part, like:

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

For text quotes I know that we can use the [...] for leaving out part of the quote.

But what do we use in the case of programming code quotes?

Solution

Lean has sorry, which is even syntactically-valid if the omitted part is an expression, as it is here. So if you are writing an exercise in Lean and you want provide a partially-filled answer that the reader could try to fill in:

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

It differs from _ in that Lean will not try to fill in the blank when you use sorry.