[rafaelRiv]

I program very often in idris2 and I cannot agree more. LLMs tend to take the least effort possible to the point where most of the time, llms are just not useful to program with dependent types. At least, not yet

[vatsachak]

Have you tried giving them the types you want and then have them auto complete? They are pretty good at a auto completing abstractions

[rafaelRiv]

I do but I have no guarantee that the llms will make a sane implementation of the types

[dleink]

You still want to write/review/refine the types yourself.