FFI : m_foreach in lean_external_class

Stream: lean4

[He-chien Tsai]

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

[Mac]

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]

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?