Skip to main content

Questions tagged [structure]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
0 votes
1 answer

How does one define a structure with the ext theorem in Lean 4?

I get this error: unknown attribute [ext] and my code is literally a copy paste of the code from mathematics in lean: ...
Charlie Parker's user avatar