Structuring Code / importing Modules

Stream: new members

[Philipp]

I'm currently solving Advent of Code in Lean (but just programming, no proving) and it would be helpful to have a Common file with parsing helpers etc.

So I have Common.Lean:

namespace Common

def String.parseNatList (s : String) : List Nat :=
  ((s.trim.splitOn " ").map String.toNat?).filterMap id

How do I access this in Day05.lean:

import AdventOfCode.Common
open Common (String.parseNatList)

-- these work:
#check String.parseNatList
#eval String.parseNatList ""

-- these fail:
#eval "".parseNatList

def readSeeds (s : String) : List Nat :=
  ((s.splitOn ":").get! 1).parseNatList
-- invalid field 'parseNatList', the environment does not contain 'String.parseNatList'

How do I import it correctly?

[Martin C. Martin]

It looks like you don't have an end Common at the end of your Common.lean file?

[Martin C. Martin]

Also: great that you're doing Advent of Code! I'm doing it too, but in Python, not Lean.

[Kyle Miller]

Martin C. Martin said:

It looks like you don't have an end Common at the end of your Common.lean file?

That's fine, in Lean 4 it's optional

[Kyle Miller]

Just remove namespace Common in your Common.lean. This is causing your function to be Common.String.parseNatList

[Kyle Miller]

Unlike Python or Java, modules and namespaces are orthogonal concepts for organizing code in Lean. You don't need to have a module to have the same namespace.

[Kyle Miller]

I'll say that it's interesting that open Common (String.parseNatList) doesn't enable dot notation. I'm not sure if that's a bug or intentional...

[Kyle Miller]

@Philipp Thanks, I went ahead and reported this as an issue. lean4#3031

[Philipp]

Kyle Miller schrieb:

Just remove namespace Common in your Common.lean. This is causing your function to be Common.String.parseNatList

that's what I did as a workaround :) Still looking for lean best practices - maybe I should just not use namespaces until I actually need them.

[Kyle Miller]

Your suggestion might become a best practice one day, but for now we all just stick extension functions right into the namespace of the object you're extending (like String here)