说【一般】是因为 MiniAgda，Agda，MiniTT 都没存参数类型，但是也有例外，比如 Idris 存了。