"Core language" refers to the exported well-typed terms that can be evaluated (or reduced).
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.