lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

doc: use {b_}obj_{arg,res} consistently in lean.h

Open digama0 opened this issue 2 years ago • 0 comments

Documentation regarding the borrowing convention of arguments and return values for C functions in lean.h and related files is very important for FFI writers to be able to use lean_inc and lean_dec correctly. This PR replaces all uses of object * in arguments and returns with the appropriate typedef from b_lean_obj_arg, u_lean_obj_arg, lean_obj_arg , b_lean_obj_res, lean_obj_res. I have reviewed all annotations added here. Functions that use lean objects in "weird" states like alloc/free have been left as lean_object *.

One aspect which I could use some guidance on is whether to use lean_obj_arg or obj_arg in object.cpp and other cpp files which have both spellings available. The existing code seems to use them inconsistently. In this PR I opted to keep the signature spelled the same between the header file and the cpp file, meaning that functions would use the lean_ spelling when the declaration is in lean.h and the lean:: one for things in object.h.

digama0 avatar Aug 27 '23 06:08 digama0