Constructive and Non-Constructive Proofs in Agda (Part 1): Logical Background

Hi! I’m Danya Rogozin, and I work at Serokell on a blockchain framework called Snowdrop.. I would like to tell you about constructive and non-constructive proofs in a proof assistant and functional …...