lean: the type model, subtyping, and a self-checking oracle - #760

Draft

lwshang wants to merge 7 commits into

Commits on Aug 14, 2026

lean: slice 1 -- types, field-id hash, subtyping, and a self-checking oracle

lwshang
and
claude
committed
70434b8
docs: relax the policy boundary to location, and correct what slice 1 disproved

lwshang
and
claude
committed
4eefc45

Commits on Aug 25, 2026

fix(lean): swap the subtype memo with the tables in the parameter premise

lwshang
and
claude
committed
bbc767b

Commits on Aug 26, 2026

lean: flatten the type language so the table is the only recursion

lwshang
and
claude
committed
47cf13e
lean: rename TypeExpr.lean to Types.lean, and record Slot/Composite in crates/

lwshang
and
claude
committed
28a6ecd
lean: record assumed pairs instead of carrying their complement

lwshang
and
claude
committed
78983a2
lean: enforce two spec rules, fix two citations, wire `lake test`

lwshang
and
claude
committed
639d16f