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