lean_expr_mk

Stream: lean4

[Scott Viteri]

I notice in Lean/Expr.lean there are functions like

@[export lean_expr_mk_app] def mkAppEx : Expr → Expr → Expr := mkApp

for each Expr constructor. It seems like it is being used to define native lean application like in racket but I am not sure. What is this line doing, and how would I find this out for myself?

[Sebastian Ullrich]

I don't know what "native lean application" means. This function is used by the C++ code, which you can find out by grepping for the name after export.

[Scott Viteri]

ok, I see

extern "C" object * lean_expr_mk_app(obj_arg f, obj_arg a);
expr mk_app(expr const & f, expr const & a) { return expr(lean_expr_mk_app(f.to_obj_arg(), a.to_obj_arg())); }