反轉陣列

說明

你的任務是證明自訂的陣列反轉函式與內建的List.reverse相等。

由於這個練習的性質，證明並非透過傳統的執行階段測試來檢查，而是由定理check檢查。 如果這個定理通過型別檢查，你就可以視為測試通過。

如果你在本機工作，或在 Lean 的線上遊樂場中工作，你可以透過 Lean InfoView 即時獲得回饋，了解任何定理是否成功或失敗，以及失敗的原因。 這是個非常寶貴的工具，能顯示你的證明所使用的所有區域值，以及你目前的目標。

在 Lean 中證明定理

定理證明是 Lean 不可或缺的一部分。 它讓程式設計師能夠證明程式的性質、推理程式的行為，並在型別層級編碼限制與規格。

這一章對 Lean 的定理證明了良好的入門介紹。 如果想更深入，這本書 被列為 Lean 官網上的官方資源。

Lean 提供許多策略，能自動完成證明，或證明其中的一部分。 你或許會想參考語言參考文件。

@[csimp]
theorem custom_reverse_eq_spec_reverse : @Extra.custom_reverse = @List.reverse := by
    ... -- proof here

-- now any occurrence of `Extra.custom_reverse` may now compile to `List.reverse`.