Agda is hard, I appreciate tactics so much more right now
Conversation
i have quite the opposite experience whenever i try to use lean
1
7
that's just because you're too constructivism pilled probably
1
3
more like i can't contort my brain into writing a functional program using an imperative/stack based meta language lol. i'd rather write the functional program directly
3
12
Definitely found the 'functional programming' style much easier as a beginner – took me a long time to get a feel the tactic script style (not an expert in either though). I do like that Lean 4 is hygienic at least - feels less cursed than the stuff you could do otherwise. 😅
I liked that in Lean was they gave you the option to use the functional approach too, then build up to tactics. And you can mix and match the styles pretty nicely, embedding tactic scripts in terms and vice versa.
1
I think that might be possible in Agda too – needs more people working on tactic libs though, I guess. Just felt nicer than in Coq where you have a weird separate definition thing for tactics vs terms. Maybe a relic from languages where proofs and terms really were separate?
1