18 lines
704 B
Markdown
18 lines
704 B
Markdown
# 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:
|
|
|
|
```lean
|
|
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
|