ac_refl and intro

Stream: lean4

[Jan-Mirko Otter]

Hello everyone,
I started using Lean4 a few weeks ago. Awesome product. By reading the Lean4 source code, I just found the ac_refl tactic.

However, for some reason, it does not work when the used variables are introduced using intro

Minimal example:

/- works fine -/
example (x : Nat) : x = x :=by ac_refl

/- does not work ; Error message: unknown free variable '_uniq.372' -/
example : ∀ x : Nat, x = x :=by intro x ; ac_refl

The snippet above is for the nightly, but it is the same behaviour on stable lean (using ac_rfl instead).

Same error occurs if I implement the necessary instances for Nat (.+.)

Can anyone help here?

[Patrick Massot]

I can confirm this but is still present in the most recent version, but ac_refl is spelled ac_rfl now.

[Dan Velleman]

Perhaps a withMainContext is missing?

[Patrick Massot]

I certainly sounds like some with... is missing.