iris

Small (toy) dependently typed core w. a bidirectional typechecker. It takes a named raw syntax, checks and elaborates it into a de Bruijn core and evaluates terms into semantic values, quotes them back for diagnostics and uses conversion checking to compare normal forms. The current kernel has explicit universe levels U0, U1, U2, dependent function and pair types, projections, annotations, and let

One of the checked examples is:

def depPairTy : Raw :=
  .sig "A" (.univ 2) (.var "A")

def depPairTm : Raw :=
  .pair
    (.univ 1)
    (.pi "_" (.univ 0) (.univ 0))

which elaborates to a pair whose first component is the type U1 and whose second component inhabits it