Vlákno názorů k článku Definice uživatelských datových typů v jazyku OCaml od Calculon - Od GADT je už jen krůček k závislostním...

Od GADT je už jen krůček k závislostním typům :) Tak co to bude, Agda, Coq, Lean nebo Idris?

K tomu musím ještě dorůst :-) ale asi Idris.

Jo, ten je asi nejlepší na učení. V praxi pak Lean (ten je taky víc ML-like).