-- Files begin with a module declaration, modules not implemented yet
module Tutorial


-- import Prelude  not implemented yet

-- declare a primitive type


-- declare a more complex primitive type
ptype Array : U -> U

-- declare a primitive function
pfunc alength : {a : U} -> Array a -> Int := `(x) => x.length`

