importing data.set

Stream: lean4

[Aaron Gostein]

Hi, I am new to lean and just installed lean4. I am trying to run the following code:

[Aaron Gostein]

-- Import the necessary Lean libraries
import data.set

-- Define a symbol as a basic element of the alphabet
structure Symbol :=
(value : String)

-- Define an alphabet as a set of symbols
structure Alphabet :=
(symbols : Set Symbol)

-- Define an alphabet sequence as a sequence of alphabets
structure AlphabetSequence :=
(sequence : List Alphabet)

-- Define some symbols
def symbol1 : Symbol := { value := "A" }
def symbol2 : Symbol := { value := "B" }
def symbol3 : Symbol := { value := "C" }

-- Define alphabets
def alphabet1 : Alphabet := { symbols := [symbol1, symbol2].toSet }
def alphabet2 : Alphabet := { symbols := [symbol2, symbol3].toSet }

-- Define an alphabet sequence
def alphabetSeq : AlphabetSequence := { sequence := [alphabet1, alphabet2] }

[Aaron Gostein]

But I am getting an error message: "unknown package data"

[Ruben Van de Velde]

data.set is not something you can import in lean4 (and read #backticks)

[Aaron Gostein]

Ah okay. In that case what should I be importing?
Or will I need to create the Set datatype myself?

[Mario Carneiro]

most likely file#Mathlib/Data/Set

[Ruben Van de Velde]

file#Mathlib/Data/Set/Basic

[Mario Carneiro]

that's how the renaming convention works, capitalize the components and put Mathlib in front

[Mario Carneiro]

except this one has since moved

[Patrick Massot]

Let me be more explicit: Aaron, you pasted Lean 3 code.

[Patrick Massot]

This is a completely obsolete version of Lean which is not compatible with the current Lean.

[Ruben Van de Velde]

Though lean 3 code would say set, not Set, so you've got some kind of Frankenstein's lean :)

[Patrick Massot]

So you need to stop reading whatever you are reading and look for an updated version.

[Aaron Gostein]

okay thank you!

[Patrick Massot]

Even better you can tell us what you are reading and we'll see whether we can make it disappear from internet or at least add a big warning banner.

[Aaron Gostein]

It was ChatGPT lol!

[Aaron Gostein]

I guess it doesn't know Lean4 yet because it's new

[Mario Carneiro]

ah, the frankenstein makes a lot more sense now

[Aaron Gostein]

yeah

[Aaron Gostein]

so should I write import file#Mathlib/Data/Set/Basic?

[Mario Carneiro]

yes ChatGPT really likes to write in lean 3

[Mario Carneiro]

yes

[Patrick Massot]

Aaron Gostein said:

so should I write import file#Mathlib/Data/Set/Basic?

No, you should read a book or tutorial written by a human instead of asking ChatGPT.

[Eric Wieser]

Do we need a "do not use chatGPT to lean Lean 4, it will teach some mangled hybrid of Lean 3" warning in the community "learn" page?

[Mario Carneiro]

I don't know if it needs to be phrased that strongly, but perhaps something like "be aware that ChatGPT has not seen much lean 4 code and will usually use lean 3 syntax, even when asked to produce lean 4 code"

[Aaron Gostein]

hmm this code is not working either:
import file#Mathlib/Data/Set/Basic

I'm getting "unknown package file" now

[Mario Carneiro]

import Mathlib.Data.Set.Basic

[Mario Carneiro]

that's just the linkifier syntax

[Aaron Gostein]

Ah got it! That works now. Thanks!!!