Builtin record type #26

kernel: record types
Add three new term/value constructors (RecordType, RecordIntro,
RecordProj) to Core, with custom printers for all six variants.
NbE conversion (lib/elab/unify.ml) gains an eta law for records:
when one side is a VRecordIntro and the other is a neutral,
the neutral is eta-expanded by projecting each field. Quote-back in
PartialRenaming.rename handles all three constructors with telescope
walking for VRecordType.fields. A BadProjection kernel error is added
for ill-formed projections.
surface: AST, lexer, parser, op_resolver for records
Add Record top variant and RecordLit / RecordUpdate / Proj preterms
plus PRecord pattern. Parser (lib/elab/parser.ml) adds
p_record_top mirroring p_data_top, plus a 3-way classify_lbrace
disambiguator that distinguishes record literals, copy-with-update
({ r | f = e }), and the existing pi-binder { x : T } form; field
punning ({ x } sugar for { x = x }) is resolved at parse time.
Postfix .field projection is implemented as a left-associative proj_soup
wrapping op_soup. Record patterns { f = p, ... } parse only with
explicit entries (no punning). op_resolver.ml walks all new variants
as pure pass-through. Implicit-application f {x} continues to parse;
Nat/zero qualified names continue to use /.
elab: \record top, companions, literal, projection, update, pattern, exports
Implement \record top-level elaboration via a two-phase
 GTopRecord -> KTopRecord_HaveType
continuation mirroring \data.
Each record produces five Module.t Let entries: the record
head, R/mk, one R/<field> per field, and R/elim. Companion bodies
use definitional eta to typecheck. Field-type telescope-walk uses
the Core terms from the type-checking pass (the placeholder
ctx_for_fields approach was a bug that broke dependent field types
like 'snd : B fst').