Registry · Definition VII.D22 tau-effective formalized

VII.D22 — Readout Functor

Functor R: K_τ → Expr from kernel to expressions; typed if factors through register readout; untyped if projects directly risking register conflation.

Book VII Part 1 Ch. 15

Dependency Graph

Depended on by (1)

VII.T10

Lean Formalization

Module: TauLib.BookVII.Meta.Registers

Symbol: Tau.BookVII.Meta.Registers.ReadoutFunctor