114747bb3d
Add definitional transport and congruence combinators derived from Id so equality programming isnt all raw idElim
master
imiel2026-04-19 18:06:54 +00:00
03eedd855d
Replace the listy context API with indexed lookups and explicit scope invariants
imiel2026-04-19 17:35:19 +00:00
28c9f2f9f8
Replace hardcoded universe levels with a proper level language and constraint solving
imiel2026-04-19 15:50:59 +00:00
963c9f3e94
Split neutrals from canonical values so stuck eliminators arent encoded via constructor overloading
imiel2026-04-19 15:03:40 +00:00
bb002a4d92
Rehydrate binder names during quoting so diagnostics stop hemorrhaging raw de bruijn indices
imiel2026-04-19 14:22:34 +00:00
85be37b1d6
Write Nat/Unit/Empty/Id Eliminators Through NbE and Bidir Elaboration
imiel2026-04-19 13:55:05 +00:00
imiel