Introducing an instance in term-mode.

Stream: general

[Adam Topaz]

In tactic mode, we can introduce a typeclass instance using letI. Is there an analogue that does something similar in term mode? One can, of course, add many @'s and manually put in a named instance when needed, but this gets annoying.

Here is an example of something I would like to be able to do. The first definition fails because lean can't find a monoid instance for N.
The other two definitions work, but are more cumbersome.

import algebra

variables (M : Type*) [monoid M]

def foo0 : M → Prop := λ x,
  ∀ (N : Type*) [monoid N]
    (g : M →* N), g x = 1 -- fails to find the monoid instance for N.

def foo1 : M → Prop := λ x,
  ∀ (N : Type*) (h : monoid N),
  begin
    letI := h,
    exact ∀ (g : M →* N), g x = 1
  end -- this works

def foo2 : M → Prop := λ x,
  ∀ (N : Type*) (h : monoid N)
    (g : @monoid_hom M N _ h), g x = (@monoid.to_has_one _ h).one -- this works

[Johan Commelin]

Nope, the idiom is by letI := h; exact _

[Johan Commelin]

Will/shall/can/must be fixed in :four_leaf_clover:

[Adam Topaz]

I see. Thanks.

[Adam Topaz]

Yeah, so I can make foo1 a bit shorted like this, but it still just tactic mode :(

def foo1 : M → Prop := λ x,
  ∀ (N : Type*) (h : monoid N), by letI := h; exact ∀ (g : M →* N), g x = 1

[Eric Wieser]

Is there a trick to define notation to achieve this?