The UX in Agda Is a Lot Smoother, Right?

The interface to the holes in Agda is a lot nicer than in Haskell. I think there's also like a lot more things in scope, usually, because you're not working on a specific proof,. You're kind of writing a big program. Is that something you've been thinking about as well? Yeah.