Share good ideas and conversation.

__Login__or__Take a Tour__!dyad · 240 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