Curator of Mastodon.art fediblock :newt: on Nostr: Andrew Scathach agda has never been intended as a haskell replacement. It's a niche ...

Andrew (npub1l4z…cyh6) Scathach (npub1lc8…92pf) agda has never been intended as a haskell replacement. It's a niche tool and works mostly as a proof assistant. I don't think that majority of agda code is even supposed to run. If it typechecks, then the proof is correct.