Zulip Chat Archive

Stream: lean4

Topic: implicit lambdas

Daniel Selsam (Apr 13 2021 at 16:26):

@Mario Carneiro FYI

example (P : Prop) : ∀ {p : P}, P := by
  have _ from 1
  apply id -- works now

works now thanks to https://github.com/leanprover/lean4/commit/bf4b9b0ccd7688d3d4024bc06a0c7a3b207124bd, though

example (P : Prop) : ∀ {p : P}, P := by
  exact id -- still fails

still fails, since exact does not indirect through refineLift

Daniel Selsam (Apr 13 2021 at 16:27):

I think the new behavior makes sense.

Last updated: Dec 20 2023 at 11:08 UTC