Lean 4 FFI memory layout for constructors with mixed object and scalar fields. Use when: (1) assertion violation "i < lean_ctor_num_objs(o)" accessing constructor fields, (2) assertion violation "offs
.claude/skills/lean4-ffi-constructor-layout/SKILL.md(main)