a thoughtful web.
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