Comment Comment by be5invis So where is the famous Idris elaborator? Where are the universes? Where’s inductive types? Where are they? parent be5invis 9 years ago