Prop Structure

Stream: lean4

[Marcus Rossel]

IIRC, to declare a structure that lives in Prop, all fields must also be propositions.
I currently find myself wanting to define a few propositions which are of the form \exists a b c, p \and q \and r \and s. Using \exists for this is kind of painful as all of the terms in the conjunction are unnamed. Using a custom inductive type for this basically suffers from the same problem, as it doesn't generate projections for p, q, etc.
Would it be an option to have Prop-structures with non-Prop fields and just not generate projections for them?

[Reid Barton]

In Lean 3 it works just like that--does it not work in Lean 4?

[Henrik Böving]

No the kernel will complain that:

(kernel) failed to generate projection 'Foo.x' for 'Foo', type is an inductive predicate, but field is not a proposition

[Henrik Böving]

(though that might of course be fixable)

[Sebastian Ullrich]

I believe this is the same in Lean 3. If there was no projection for a, how would the type of p's projection refer to it?

[Sebastian Ullrich]

You can always declare a structure for p \and q \and r \and s parameterized over a b c though

[Reid Barton]

If I understand what's going on, it sounds like the only difference is in some cases you can't use the structure syntax but you can use the inductive syntax to achieve the same thing.