CoqStock refers to chicken stock and is a base (standard library) for our "curry".
This library is for proofs, tactics, classes, definitions, etc. that we wish existed in the Coq standard library. This wish might come from being naive, since we are still learning Coq, or it might be a legitimate wish. We aren't here to judge.
The requirement is that it is has nothing to do with regular expressions, but we possibly want to use it to help us prove things about regular expressions.
Examples include:
- tactics for list
- proofs about list_set
- comparable class
- a semi ring that includes orb