What is `_obj`?

Stream: lean4

[Arthur Paulino]

Looking at this line we see:

def objectType : Expr        := mkConst `_obj

We also noticed that having a prelude file and having a simple def id (a : α) : α := a in it creates this in the environment:

unsafe def id._rarg._cstage2 : _obj -> _obj :=
  fun (a : _obj) => a

What does _obj mean?

[Sebastian Ullrich]

It's the IR representation of the last category (+Nat) from https://leanprover.github.io/lean4/doc/dev/ffi.html#translating-types-from-lean-to-c