Zulip Chat Archive

Stream: Is there code for X?

Topic: pi_instance for products

Adam Topaz (Dec 08 2020 at 16:25):

Do we have something like pi_instance for binary products?

Eric Wieser (Dec 08 2020 at 16:31):

I assume you don't mean docs#pi.has_mul

Adam Topaz (Dec 08 2020 at 16:33):

Not exactly. There's this pi_instance tactic that makes instances (usually of algebraic nature) for Pi-types automatically. I want something which is even simpler -- a tactic that does this for binary products (which mathematically are a special case of Pi-types, but not definitionally so).

Eric Wieser (Dec 08 2020 at 16:37):

Got it - so you want a prod_instance tactic for building the proofs with instances over prod A B?

Eric Wieser (Dec 08 2020 at 16:37):

(deleted)

Eric Wieser (Dec 08 2020 at 16:38):

Based on the content of algebra/group/prod we don't have one: https://github.com/leanprover-community/mathlib/blob/3996bd428d1758fa6f790a2453bd679e10ad1897/src/algebra/group/prod.lean

Yury G. Kudryashov (Dec 09 2020 at 02:24):

Note that currently pi_instance generates extra ids, so we use it only to prove properties.

Last updated: Dec 20 2023 at 11:08 UTC