3. Operational Semantics
The operational semantics is a labelled transition system with five judgment forms and 18 inference rules (Section 4 of the paper). All rules are encoded as inductive propositions in Lean 4.
The operational semantics is a labelled transition system with five judgment forms and 18 inference rules (Section 4 of the paper). All rules are encoded as inductive propositions in Lean 4.