Zulip Chat Archive

Stream: lean4

Topic: lean_expr_mk


view this post on Zulip Scott Viteri (Apr 08 2021 at 17:52):

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?

view this post on Zulip Sebastian Ullrich (Apr 08 2021 at 17:58):

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.

view this post on Zulip Scott Viteri (Apr 08 2021 at 18:02):

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())); }

Last updated: May 18 2021 at 23:14 UTC