Hacker GitHub

← All repos

AndrasKovacs/smalltt

View on GitHub ↗ ★ 611 Lean

Demo for high-performance type theory elaboration

3 mentions on Hacker News by 2 people: 0 stories, 3 comments · first 2020-01-20 · latest 2022-09-14

Mentions per year 3 mentions · busiest year 2022 (2)
20082026
AllStoriesComments NewestTopOldest
  1. …merely because they are based off people in the Blockchain space is equally as befuddling. Try https://github.com/AndrasKovacs/smalltt if you want a system that considers the things modern systems care about: elaboration and unification.
    comment by voxl · 2022-09-14 · in The Little Prover
  2. …programs can be quite slow to compile, slower than even other dependently-typed languages (see e.g. https://github.com/AndrasKovacs/smalltt ). How much of this is intrinsic to Idris' language design and how much of it is due to lack of…
    comment by dwohnitmok · 2022-01-24 · in Idris 2: Quantitative Type Theory in Practice
  3. …but this seems like an implementation issue rather than a fundamental limitation. Efforts like https://github.com/AndrasKovacs/smalltt/blob/master/README.m... make me hopeful this is something that can be solved.
    comment by dwohnitmok · 2020-01-20 · in A game in a pure language (part 1): introduction and problems with Idris