[kmill]

Many times, Decidable assumptions are added simply because they appear in the terms in a theorem statement, and doing so makes applying such a theorem easier. There's the technical annoyance that Decidable instances are equal but not necessarily defeq, so if the wrong instances are present (such as the classical ones) then you need simp-like automation to rewrite instances before unifying. Maybe this is what you're seeing?

There have also been attempts to make polynomials computable, which peppers everything with decidability, but it's not a good data type for real large-scale computations, so it's not clear what the future is there. Maybe the defeqs are worth it, I don't know.

Re constructibility, this is all at too high of a level to really know what you're talking about, or why it's beneficial to write proofs themselves in a certain way. I'm not really even sure what you mean by "constructive". To me, I see no problem with writing a recursive definition that requires a non-constructive proof of termination by well-founded recursion -- is that constructive to you?

[zozbot234]

AIUI, the fact that well-founded recursion is encoded as "noncomputable" in Lean is just a wart/quirk of that particular system; it can be justified in dependent type theory which is quite constructive and used by other systems such as Coq.

[kmill]

It's not `noncomputable` in Lean though. Lots of computable functions use it.

I've read Bauer's paper before btw. I think topoi are cool, but I don't think it's a complexity worth thinking about for everyone else who isn't concerned about these things.