"Core language" refers to the exported well-typed terms that can be evaluated (or reduced).

In the core language of MiniAgda, a dependently-typed language, the parameter type of a lambda is not stored anywhere. So does in Mini-TT and Agda.

However, Idris does store lambda parameter type in its core language.

I wonder do we need/needn't to store parameter type (or, under what condition do we need/needn't to store it)?

"Core language" refers to the exported well-typed terms that can be evaluated (or reduced).

In the core language of MiniAgda, a dependently-typed language, the parameter type of a lambda is not stored anywhere. So does in Mini-TT and Agda.

However, Idris does store lambda parameter type in its core language.

I wonder do we need/needn't to store parameter type (or, under what condition do we need/needn't to store it)? Because according the surface syntax of all these languages, they don't have lambdas with their parameters explicitly-annotated. For Idris here's a link showing that Idris does not have lambda with type annotation.