Zulip Chat Archive

Stream: lean4

Topic: ac_refl and intro


Jan-Mirko Otter (Aug 24 2022 at 07:34):

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 (Aug 24 2022 at 07:48):

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

Dan Velleman (Aug 24 2022 at 17:52):

Perhaps a withMainContext is missing?

Patrick Massot (Aug 24 2022 at 18:09):

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


Last updated: Dec 20 2023 at 11:08 UTC