Nice, nice. I'll definitely frequent that github for a while.
Name:
Anonymous2015-03-24 3:14
That shit is 117 lines long.
Name:
The Peanist2015-03-24 5:13
decBuzzy : (n : Nat) -> Dec (Buzzy n) decBuzzy Z = Yes ZeroBuzzy decBuzzy (S Z) = No oneNotBuzzy decBuzzy (S (S Z)) = No twoNotBuzzy decBuzzy (S (S (S Z))) = No threeNotBuzzy decBuzzy (S (S (S (S Z)))) = No fourNotBuzzy decBuzzy (S (S (S (S (S k))))) with (decBuzzy k) decBuzzy (S (S (S (S (S k))))) | (Yes prf) = Yes (Buzz prf) decBuzzy (S (S (S (S (S k))))) | (No way) = No (buzzOff way)
>>4 I hope he knows we invented a pretty good notation for numbers already.
Name:
Anonymous2015-03-24 17:34
>>6 Why don't they use n+k patterns and let the compiler translate them to iterated successors?
Name:
Anonymous2015-03-24 19:08
>>4 What if the "buzzy" property was defined not as divisibility by 5, but as divisibility by 297? Would he need 297 case analysis lines then?
Name:
Anonymous2015-03-24 19:22
Dependently-typed programmers sure get a lot of S!
Name:
Anonymous2015-03-24 20:24
>>8 Yes. There is no other way in dependently typed languages.
Name:
Alexander Dubček2015-03-24 23:56
Dependently typed doubles.
Name:
Anonymous2015-03-26 20:51
Totality matters not because it guarantees typechecking terminates, but because it means you don't have to evaluate certain things at all. In a total language, if you have a proof that two types are equal then you can transport values between them, preserving type safety, without any runtime cost. Without totality, you have to evaluate your proofs before you can trust them.
>>19 Can anyone explain Coq? I have no idea how to use it, I know a good deal of math and a bit of Haskel. Do I learn more haskell before I touch Coq or what?
>>21,23 Immature Coq users or... ? I don't think you have ever touched Coq before in your lives. I'd rather get an answer from a person with experience in Coq.
Name:
Anonymous2015-03-27 8:01
I don't think you have ever touched Coq a person with experience in Coq.
I have 30-year experience in Coq and my arm strength is great. However touching Coq all day is not conductive to programming. You can't write an app while touching Coq. Coq is more like a distraction.
Name:
Anonymous2015-03-27 8:53
>>24 Coq has penetrated my research in ways I never thought possible, probing deep into my curiosities with the relentless determination only a machine could muster. I always thought some areas of mathematics could never be reached, but Coq gets in there and hits it hard with everything its got for me every night.
Name:
Anonymous2015-03-27 9:21
THE COQ CLUB. =============
The Coq Club moderated mailing list is meant to be a standard way to discuss questions about the Coq system and related topics. The subscription link can be found at http://coq.inria.fr/community.
The topics to be discussed in the club should include:
* technical problems;
* questions about proof developments;
* suggestions and questions about the implementation;
* announcements of proofs;
* theoretical questions about typed lambda-calculi which are closely related to Coq.
For any questions/suggestions about the Coq Club, please write to coq-club-request@inria.fr.
>>27 None of the bullets was about newb-friendly questions. I am not going to mail these guys
Name:
Anonymous2015-03-27 9:31
Moreover, some users of Coq have published various documents that may be useful both to beginners and advanced users of Coq:
the Coq'Art, the first book dedicated to the Coq proof assistant (Yves Bertot, Pierre Castéran, 2004, Chinese version in 2009); Software Foundations, a Coq-based textbook on logic, functional programming and foundations of programming languages (Benjamin Pierce et al, 2007, with regular updates); Certified Programming with Dependent Types, a textbook about practical engineering with Coq (Adam Chlipala, 2008); Video tutorials (Andrej Bauer, 2011); Preuves de programmes en coq (Video lectures in french) (Yves Bertot, 2013); a tutorial browsable interactively as a Coq file (Mike Nahas, 2014); Coq in a Hurry (Yves Bertot, 2006); an old Tutorial, which is a commented interactive session which introduces basics on terms, proofs, and tactics (Gérard Huet, Gilles Kahn and Christine Paulin-Mohring); a Tutorial on Recursive Types in Coq (Eduardo Giménez, Pierre Castéran, 2006) and the associated examples; a bunch of Frequently Asked Questions; Cocorico!, the Coq wiki; A Gentle Introduction to Type Classes and Rewriting in Coq (Pierre Castéran, Matthieu Sozeau, 2012) and the associated examples for Coq 8.3 and 8.4.
Name:
Anonymous2015-03-27 9:35
>>29 Maybe Coq in a Hurry will be useful. I'll check it out this weekend.
The Coq Club moderated mailing list is meant to be a standard way to discuss questions about the Coq system and related topics. The subscription link can be found at http://coq.inria.fr/community.
The topics to be discussed in the club should include:
* pleasing the Coq type system
* taking in the girth of Coq's tactics
* swallowing the load of Coq's output format
* riding Coq until it gives you what you want
* theoretical questions Coq can penetrate and cover in enlightening fluid to lubricate further research and impregnate new fields.
For any questions/suggestions about the Coq Club, please write to coq-club-request@inria.fr.
