> Programs in most DT languages run directly (Lean, Idris, Adga, etc), code extraction is a Coq thing (and Isabelle, but Isabelle does not use DT). Some languages have type erasure, some don't. Some are explicitely concerned about type erasure (Idris), some don't.
Lean has proof irrelevance which means that any information that may be contained within the "proof" or "logical" part of the program is erased at runtime. It amounts to largely the same thing.
Lean has proof irrelevance which means that any information that may be contained within the "proof" or "logical" part of the program is erased at runtime. It amounts to largely the same thing.