Here's the quote justifying my weird username. It's from Dedekind's "Was sind und was sollen die Zahlen" ("What are numbers and what are they good for?").
"But I know that, in the shadowy forms which I bring before him, many a reader will scarcely recognize his numbers which all his life long have accompanied him as faithful and familiar friends; he will be frightened by the long series of simple inferences corresponding to our step-by-step understanding [ger. Treppenverstand], by the matter-of-fact dissection of the chains of reasoning on which the laws of numbers depend [...]"
The term thus characterizes our capability of reasoning to be restricted to discrete steps and is meant to contrast the rather informal, intuition-based proofs that were the norm back in 1888 when the paper was written.
It is also a very funny sounding word.
Haha, simply compute the bound of the depth of the reduction tree. Surely that can't be that hard...
in other maths u have to explain ur proofs to the reader who can think, but agda is brain empty
Actually, I can constructivize parts of it. Probably enough to get the things I actually care about to be constructive...
studying mathematical logic • ex-CS student • interested in type theory + constructive mathematics + game semantics + non-economic games • will only write code that doubles as proof
trans rights + against all unjust hierarchies