Zulip Chat Archive
Stream: lean4
Topic: error puzzle
Damiano Testa (Mar 12 2024 at 02:32):
In the spirit of Patrick's recent post, here is another puzzle: can you guess the error in the code below, without using Lean?
example : False ↔ False :=
⟨fun h => by cases h, fun h => by cases h⟩
Trivia: there are a couple of porting notes about this.
Kyle Miller (Mar 12 2024 at 02:46):
Damiano Testa (Mar 12 2024 at 02:54):
Correct!
Eric Rodriguez (Mar 12 2024 at 03:00):
Kyle Miller said:
Mario Carneiro (Mar 12 2024 at 16:28):
By the way, use
has a similar issue
Damiano Testa (Mar 12 2024 at 23:40):
Another one: what is the error in
example (x : Bool) (h : false ∨ true) : True := by
match x with
| true => rcases h with ⟨⟩
| false
exact .intro
exact .intro
| false => exact .intro
Last updated: May 02 2025 at 03:31 UTC