OtherContents
List of other pages stored on this Wiki.
- QuickSort: an implementation of quicksort in Coq.
- InductiveFiniteTypes or alternatively FixpointFiniteTypes.
- An other version of InductiveFiniteTypes not using nat.
- ListOfPredecessors for binary numbers.
- ExcludedMiddleOnNegativeFormulasFromCoqRealAxioms
- A proof of Lagrange's Theorem.
- A proof that there are not finitely many primes.
- 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
- Monads in Coq
- A short tutorial on extraction
- Math Classes: Mathematics using TypeClasses
- A discussion about Coq Style.
- A discussion suggesting preferring Set to Prop.
- 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 intensional equality.
- How should I organize large inductive proofs?
- How can use the module system effectively?
- Another QuickSort: an implementation of quicksort in Coq using Program and definitions from the standard library.
- Information about Coq's source code.
- How do TypeClasses work?
- How can I build the CoqIDE under Mac OS X without X11
- How can I input unicode characters for Coq independently of my editor using XCompose (X graphical servers only) or the TeX input method (Unix systems).
- HowToContributeToTheStandardLibrary?
- How can I avoid non-instantiated existential variables with eauto?
- What exactly does simpl do?
- How can I make Coq always print universes?
- Resources for Coq Newbies
- How does the pattern match syntax work?
- How does dependent inversion work?
- When using
eapply, how can I instantiate the question marks? - Why doesn't Coq support extension equality? (Why can't I prove
forall x, f x = g x) -> f = g?) - Why can I eliminate False (a
Prop) when constructing a member ofSet? - How does the fix tactic work?
- Why do I get "Error: Abstracting over the term ... leads to a term which is ill-typed" when rewriting with equalities?
- Where can I see other examples of formalization and verification?
- CoqIDE crashes in KDE. Help!
To the extent possible under law, the contributors of the Rocq wiki have waived all copyright and related or neighboring rights to their contributions.
By contributing to the Rocq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.