What is _kernel_fresh ?

Stream: lean4

[Tomas Skrivan]

I have a buggy tactic and I'm getting an error

unknown free variable: _kernel_fresh.7154

I have never seen this before. When is _kernel_fresh being created? What does it mean?

Not sure if it matters but I'm working on a modified version of simp. Are _kernel_fresh fvars created somewhere in simp?

[Kyle Miller]

It looks like it's a name prefix used by the kernel when it needs to do its own version of withLocalDecl, for example to infer the types of lambdas or lets, or when doing defeq checking of pi types, or when doing eta expansion.

Look for uses of m_ngen in src/kernel/type_checker.cpp

[Tomas Skrivan]

Interesting, I wonder how I managed to screw up so badly that I confused the kernel.