lean - Type 和 Type* 有什么区别？

Question

我Type*在这个项目中看到了一些实例。跑步#check Type*给予Type u_1 : Type (u_1+1)和#check Type给予Type : Type 1。

搜索语言参考和ingCtrl-F表达式章节似乎没有提供任何关于Type*. 从概念上讲，它是用来做什么的？另外，如果可能的话，我链接的项目中使用了什么？

（*很难搜索，如果这是重复的，请见谅。）