Abstract. Type checkers for dependent types need to evaluate user defined functions during type checking. For this, current implementations typically use an interpreter, which has drawbacks. We show, how at this stage compiled code can be used for a language with lazy evaluation.