How does the Lean4 work behind the scenes

Stream: new members

[Jeff]

Coming from a computer science background, I'm curious how Lean4 actually works behind the scenes for type checking. My assumption is that its similar to how expressions in Lisp would evaluated using a stack machine but I'm confused how type checking would work for more complicated user defined types like inductive types.

Is there any documentation or resources available that explain how lean4 works behind the scenes?

Thanks

[Markus Himmel]

You might be interested in the book Type Checking in Lean 4.

[Jeff]

Thanks I'll check it out