OtherContents

List of other pages stored on this Wiki.

== Coq Pearls ==

• QuickSort: an implementation of quicksort in Coq.
• InductiveFiniteTypes or alternatively FixpointFiniteTypes.
• ListOfPredecessors for binary numbers.
• ExcludedMiddleOnNegativeFormulasFromCoqRealAxioms
• A proof of LagrangesTheorem.
• A proof that there are NotFinitePrimes.
• SquareRootTwo: A very short proof that the square root of 2 is non rational.
• UntypedLambdaTerms: various data structures for implementing the untyped lambda calculus in Coq.
• ExistsFromPropToSet: Existential implies Sigma for decidable properties on {{{nat}}}.
• HandMul: A fun way of doing multiplication by hand
• AUGER_Monad
• AUGER_ExtractionTuto
• MathClasses: Mathematics using TypeClasses

== Discussion ==

• A discussion about CoqStyle.
• A discussion suggesting ExistsConsideredHarmful.
• What is the difference between Require_Import_and_Require_Export?
• Do objects living in Prop ever need to be evaluated? See PropsGuardingIotaReduction.
• A discussion about IntensionalEquality.
• How should I Organizing Large Proofs?
• How can use the ModuleSystem effectively?

== Threads to remove ==

• http://www.lri.fr/~sozeau/research/russell/quicksort.html: an implementation of quicksort in Coq using Program and definitions from the standard library.
• Information about TheSource.
• How do TypeClasses work?
• How can I BuildingCoqOnMac
• How can I input unicode characters for Coq independently of my editor using XComposeAndNotations (X graphical servers only) or the TeXInputMethodForUnicodeNotations (Unix systems).
• HowToContributeToTheStandardLibrary?
• How can I avoid http://pauillac.inria.fr/pipermail/coq-club/2007/003186.html?
• What exactly does simpl (tactic) do?
• How can I make Coq PrintingUniverses?

== Threads to update/remove ==

• CoqNewbie
• How does the MatchAsInReturn syntax work?
• How does DependentInversion work?
• When using eapply, how can I ExistentialVariablesInEapply?
• Why doesn't Coq support extensional_equality? (Why can't I prove forall x, f x = g x) -> f = g?)
• Why can I FalseEqAcc (a Prop) when constructing a member of Set?
• How does the Fix (tactic) work?
• Why do I get "Error: Abstracting over the term ... AbstractingOverTheTermLeadsToATermWhichIsIllTyped" when rewriting with equalities?
• Where can I see other examples of FormalizedAndVerified?
• CoqIDE_crashes_under_KDE