Good ideas and conversation. No ads, no tracking. Login or Take a Tour!
dyad · 1723 days ago · link · · parent · post: Proving the relationship between the golden ratio and the Fibonnaci numbers in Coq
What's your process of learning Coq? I have to confess that 'proof automation' is one of those shortcomings I never overcame. Even going through your well-documented code took me a shameful amount of time, and that's after you've done all the heavy lifting. Agreed on Idris, but, per your recommendation back from IRC dwelling days, I found Type-Driven Development with Idris by E. Brady as much more accessible. In this case, it means "I went farther into it than into any Coq tutorial". :P