Compilation errors in simpleTypes.lean

Stream: lean4 dev

[Yuri de Wit]

I am trying to get tests/playground/simpleTypes.lean compiled in my local clone but I can't seem to get past the following error (in vscode):

def test (declName : Name) : MetaM Unit := do
  IO.println s!"{declName} : {← ppExpr (← getDeclLCNFType declName)}" -- ERROR : unknown identifier 'getDeclLCNFType'

I have successfully built the latest (fea65d9) using the build instructions in the lean4 manual. I have also set elan overrides for ./ and ./src to stage1 and stage0, respectively (Lean.versionString returns "4.0.0, commit fea65d99345d959ac58cf410b31fafaaa59ded64").

I even tried to manually import Lean.Compiler.LCNF in sympleTypes.lean to make sure the module containing getDeclLCNFType was part of the build.

Any ideas?

[Leonardo de Moura]

You need to import Lean and open the relevant namespaces.

import Lean

open Lean Meta Compiler LCNF

def test (declName : Name) : MetaM Unit := do
  IO.println s!"{declName} : {← ppExpr (← getDeclLCNFType declName)}"

#eval test ``Lean.Meta.isExprDefEqAuxImpl

[Yuri de Wit]

Thanks. Stupid me ...

Is this something you all are doing manually at this point?

[Leonardo de Moura]

Is this something you all are doing manually at this point?

Not sure I understood the question. Some people suggested we include in the "unknown identifier" error messages suggestions for missing namespaces and imports. I think this would be a nice feature, but it is not implemented yet.

[Yuri de Wit]

Sorry, what I meant is that the committed version of simpleTypes.lean does not open LCNF: I had to add it manually. So this is something you and Henrik must be doing manually too, I suppose.