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