imiel 114747bb3d Add definitional transport and congruence combinators derived from Id so equality programming isnt all raw idElim

2026-04-19 18:06:54 +00:00

..

Check.lean

Replace the listy context API with indexed lookups and explicit scope invariants

2026-04-19 17:35:19 +00:00

Context.lean

Replace the listy context API with indexed lookups and explicit scope invariants

2026-04-19 17:35:19 +00:00

Eval.lean

Replace hardcoded universe levels with a proper level language and constraint solving

2026-04-19 15:50:59 +00:00

Examples.lean

Add definitional transport and congruence combinators derived from Id so equality programming isnt all raw idElim

2026-04-19 18:06:54 +00:00

Level.lean

Replace hardcoded universe levels with a proper level language and constraint solving

2026-04-19 15:50:59 +00:00

Pretty.lean

Replace hardcoded universe levels with a proper level language and constraint solving

2026-04-19 15:50:59 +00:00

Syntax.lean

Replace hardcoded universe levels with a proper level language and constraint solving

2026-04-19 15:50:59 +00:00

Value.lean

Replace hardcoded universe levels with a proper level language and constraint solving

2026-04-19 15:50:59 +00:00