Stream: new members

Topic: instance in condition

Adrián Doña Mateo (Mar 30 2021 at 12:24):

Hi. Trying to define an induction principle for finite groups I've run into the following problem. It seems like one cannot introduce an instance in the condition of a lemma. I believe this is to do with Lean not updating the instance cache inside a proof. Is there any way to get this to work (perhaps using some tactics from here)? I realise I could simply have (hα : has add α) and then provide it manually when it is needed, but I would like to avoid that.

example (h : Π (α : Type*) [has_add α] (a : α), a + a = a) : true := trivial
-- failed to synthesize type class instance for has_add α


Kevin Buzzard (Mar 30 2021 at 12:26):

import tactic
example (h : Π (α : Type*) [has_add α] (a : α), by exactI a + a = a) : true := trivial


Adrián Doña Mateo (Mar 30 2021 at 12:29):

Oh, never thought it'd be that easy. Thanks!

Last updated: May 14 2021 at 07:19 UTC