Notes on λRC IR in Lean

λRC is not a particular version of the IR. Is it the same IR as λpure, but with dec (var : obj) inc (var : obj) instructions and @& (reference marker) inserted.

In this sense, Lean 4 is a untyped, interpreted and compiled language with a sophisticated syntax translation frontend.

Relevant files in lean4 repo:

src/library/compiler/ir.h
src/Lean/Compiler/IR/Basic.lean
src/library/compiler/ir_interpreter.h

To see generated IR, put set_option trace.compiler.ir.rc true into Lean code and see it in the InfoView.