Zulip Chat Archive

Stream: new members

Topic: Sets in Mathlib4

Jonathan Whitehead (May 13 2023 at 00:19):

Hey all,

I'm just getting started and I keep getting a type error when I'm just trying to define something as simple as a subset. I tried to do it similar to the lean3 tutorial but this is what I get:


Can someone explain to me how to fix this? Moreover, can someone explain to me the process of solving type errors like this in the future. For example, it says "type expected, got ... (set U : ?m.0 PUnit)". I don't know how to interpret this error. I don't know what the ?m.0 PUnit means or how to resolve something like this.

Heather Macbeth (May 13 2023 at 00:45):

Capital s! Set

Jonathan Whitehead (May 13 2023 at 00:54):


Last updated: Dec 20 2023 at 11:08 UTC