Field is a member of a Struct or Union. It is used when creating a Struct or Union and accessing its members.

See documentation of LeanGccJit.Core.Field, and the C API documentation for gcc_jit_field.

@[extern lean_gcc_jit_context_new_field]

opaque LeanGccJit.Core.Context.newField (ctx : LeanGccJit.Core.Context) (location : Option LeanGccJit.Core.Location) (type : LeanGccJit.Core.JitType) (name : String) : IO LeanGccJit.Core.Field

Construct a new field, with the given type and name.

@[extern lean_gcc_jit_context_new_bitfield]

opaque LeanGccJit.Core.Context.newBitField (ctx : LeanGccJit.Core.Context) (location : Option LeanGccJit.Core.Location) (type : LeanGccJit.Core.JitType) (width : Nat) (name : String) : IO LeanGccJit.Core.Field

Construct a new bit field, with the given type width and name.

Note

The parameter width must be a positive integer that does not exceed the size of type.

@[extern lean_gcc_jit_field_as_object]

opaque LeanGccJit.Core.Field.asObject (field : LeanGccJit.Core.Field) : IO LeanGccJit.Core.Object

Upcast from field to object.