What are /r/agda's favorite Products & Services?

From 3.5 billion Reddit comments

FYI, Coq's standard library provides the excluded middle (LEM) as an optional axiom (postulate in Agda-speak, i.e. your 2nd option) and derives a bunch of lemmae from it which you might take as inspiration. In the linked file, you can think of Prop and Type as Agda's Set.

Be aware that as you go down the path of classical logic, computation becomes less useful since every application of LEM blocks it. Therefore, it's good practice to keep developments as constructive as possible.

Coq indeed has multiple evaluation mechanisms available, including call-by-value and call-by-name, which have different performance characteristics but evaluate terms to identical results. The same should be possible for Agda. (However, Coq's formulation of corecursion requires partially lazy semantics, so call-by-value is not fully strict. I'm not sure about Agda's.)

let, if I understand the docs correctly, is entirely syntactic sugar, so there should be no sharing. Under a lazy evaluation strategy, auxiliary definitions in where clauses would probably be shared.

Yes, Coq is also constructive. However, the standard library provides a couple of common axioms, among them LEM, whose compatibility with Coq's logic has been proven meta-theoretically (with varying degrees of rigour).

Even if you're not interested in the library ecosystem, I would still consider generalised rewriting a killer feature if you expect to do significant amounts of equational reasoning. Regarding some of the desiderata you mention in another comment:

• Coq has ProofGeneral as an Emacs interface, which works very well.
• Coq's support for syntactic extensions, notations, is more powerful than Agda's in some ways, but also less straightforward to use. It supports Unicode, but the standard library is all ASCII.

(I can't speak to the comparison with Isabelle/HOL, by the way, which may well be even better suited to your task.)