Zulip Chat Archive

Stream: lean4

Topic: FFI : m_foreach in lean_external_class


He-chien Tsai (Jun 09 2022 at 13:40):

What's m_foreach in sample code supposed to be? Only two clues is at here and here.

Mac (Jun 09 2022 at 16:16):

I don't see a use of m_foreach in the sample code you linked. However, if you are just generally curious, m_foreach is a field of lean_external_class that is used to iterate over the nested lean objects in an Lean external object. For example, if the struct you are wrapping has fields that are Lean objects (i.e., of type lean_object) you would provide a foreach method that invokes the passed function (i.e., the b_lean_obj_arg on the each of those fields).

He-chien Tsai (Jun 10 2022 at 02:25):

I mess up variables in original post, edited. In sample code, lean_register_external_class assigns S_finalize and S_foreach to m_finalize and m_foreach at here, but the only two lines which call m_foreach doesn't explicitly show what's m_foreach supposed to do, sample code literally do nothing. What's S_foreach in sample code supposed to do if it has nested objects?


Last updated: Dec 20 2023 at 11:08 UTC