Track HLevels of Sets and Theories#40

Merged

olynch merged 11 commits into

mainfrom

coln-compiler/hlevels

Jun 25, 2026

Commits on Jun 25, 2026

Initial hlevels work

mvr
authored and
olynch
committed
Sort -> MLevel

mvr
authored and
olynch
committed
Properly promote HLevel of equality type

mvr
authored and
olynch
committed
Add HUnit and HTop to HLevel

mvr
authored and
olynch
committed
Add `showlevel` debug command

mvr
authored and
olynch
committed
maxLevel should be componentwise

mvr
authored and
olynch
committed
Give FunctionVariant an HLevel instead of a separate constructor

mvr
authored and
olynch
committed
formatting
olynch
committed
Punt on `layout` for `Prop`, for now

mvr
authored and
olynch
committed
Kill `PropTheory`

mvr
authored and
olynch
committed
`hlevel.glog` -> `hlevel.coln`, put former PropTheory into Theory

mvr
authored and
olynch
committed