this is a web version of my language based on Martin-Löf type theory + W-types.

it is still incomplete.

examples

source code