A .Lean file with no imports

Stream: new members

[Martin Epstein]

In my file Queue.lean I put import Mathlib.Tactic at the top out of habit, but I don't think I actually use anything from this module. I tried deleting this statement so the file just begins with the definition "inductive Queue..." on line 1 but then Lean raised bizarre errors all over the place. I am confident the issue isnot that I really need Mathlib after all, but just that Lean expects some header code and I don't have any. What's the right way to handle this?

[Aaron Liu]

what's the errors

[Aaron Liu]

maybe it's the notation

[Aaron Liu]

can you give a #mwe

[Martin Epstein]

Oops, my attempt at a mwe didn't work.

def hello := "world"
#eval hello

compiles just fine. Here is a reduced version of Queue.lean:

-- import Mathlib.Tactic

inductive Queue (α : Type*) where
  | empty : Queue α
  | mk : α → List α → List α → Queue α

The first ) is flagged with "unexpected token ')'; expected term". The error goes away if I import Mathlib.Tactic. So I guess this definition relies on Mathlib after all.

I thought I didn't need Mathlib.Tactic because I have another much more sophisticated file (including new inductive definitions) that doesn't import it. However, that file does import Queue.lean so maybe it implicitly imports whatever Queue.lean imports.

[Aaron Liu]

you're missing import Mathlib.Tactic.TypeStar

[Aaron Liu]

file#Tactic/TypeStar

[Martin Epstein]

Aaron Liu said:

you're missing import Mathlib.Tactic.TypeStar

Ahh okay, that fixes most of the issues. Can you tell me which submodule l need in order to parse the blackboard bold N symbol as Nat?

[Aaron Liu]

that would be Mathlib.Data.Nat.Notation

[Kenny Lau]

@Martin Epstein finding notations is slightly less straightforward but it's actually still pretty straightforward, you search the symbol with quotation marks in Loogle, e.g. "Type*" and "termℕ" and then it will tell you where the notation is defined