package

Stream: new members

[edklencl]

how to import my own package. is it like python

[Kevin Buzzard]

An example from mathlib:

import Aesop.Index.Basic
import Aesop.RulePattern
import Aesop.Rule.Basic
import Aesop.Tracing
import Batteries.Lean.Meta.InstantiateMVars
import Batteries.Lean.PersistentHashSet
import Batteries.Lean.Meta.DiscrTree

[Derek Rhodes]

Modules systems can be really confusing because things are spread out over multiple files and directories. I find that it helps to look at minimal projects.

Chapter 4 of the new lean language reference is dedicated to files, modules, libraries and packages:
https://lean-lang.org/doc/reference/latest/Source-Files/#The-Lean-Language-Reference--Source-Files

[edklencl]

Kevin Buzzard said:

An example from mathlib:

import Aesop.Index.Basic
import Aesop.RulePattern
import Aesop.Rule.Basic
import Aesop.Tracing
import Batteries.Lean.Meta.InstantiateMVars
import Batteries.Lean.PersistentHashSet
import Batteries.Lean.Meta.DiscrTree

:mahjong: