AndrasKovacs/elaboration-zoo

Minimal implementations for dependent type checking and elaboration

5 mentions on Hacker News by 4 people: 0 stories, 5 comments · first 2022-09-13 · latest 2026-10-10

Mentions per year 5 mentions · busiest year 2022 (1)

20082026

All Stories Comments Newest Top Oldest

…examples elaboration of dependent types then the `elaboration-zoo` is a great thing to look at: https://github.com/AndrasKovacs/elaboration-zoo I've also got an incomplete project that aims to present a more expanded set of implementations…
comment by solomonb · 2026-10-10 · in What mathematicians should know about the Lean Theorem Prover: reliability & AI
Related: https://github.com/AndrasKovacs/elaboration-zoo
comment by etiamz · 2025-08-18 · in Typechecker Zoo
…is interested in how this works, I've found András Kovács' "Elaboration Zoo" to be a good tutorial: https://github.com/AndrasKovacs/elaboration-zoo It incrementally covers normalization by evaluation, bidirectional typechecking, basic…
comment by dunham · 2024-07-29 · in Higher-kinded bounded polymorphism in OCaml (2021)
…partial silo, I decided earlier this year to create a project similar to the [Elaboration Zoo]( https://github.com/AndrasKovacs/elaboration-zoo ) but focused on a blessed path to MLTT with a number of the desirable language features via…
comment by solomonb · 2023-06-14 · in How to implement dependent type theory I (2012)
…[2]: https://granule-project.github.io/ [3]: https://github.com/AndrasKovacs/staged [4]: https://github.com/AndrasKovacs/elaboration-zoo/
comment by bjz_ · 2022-09-13 · in A personal list of Rust grievances