[platz]

Idris & Agda are based on calculus of constructions

F* is based on type refinements and smt solver.

in theory all DT are equivalent but type refinements are less expressive in practice than CoC.

sometimes the smt solver gives up and you are in trouble.

alternatively the smt solver can provide simple refinements with less effort than CoC when it does work.