coq
coq copied to clipboard
coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive developme...
This PR is preparing the changes of documentation in #19029 and #19301, to split general concerns from specific concerns and so that either of the two PR can be merged...
### Description of the problem The gray background for lists like this should only be on the text, not the entire line. This excess formatting is distracting for short items...
This was the case in non-strict mode (via interpretation at runtime), but, in strict mode, it was instead the reference without its maximal implicit arguments. Also deprecate the old strict...
An extensionality hypothesis of the `Fix_eq` lemma is unnecessarily strong, so I have weakened it here. I've had some mild inconvenience with proving fixpoint equations, which would've been alleviated by...
In practice it seems we have many closures duplicated around. The reason is likely the fact that return clauses of pattern-matchings are compiled in the VM to closures, and most...
(and other lookup_eliminator users) For now we keep the lookup by name as a backup strategy.
This PR adds the `QGraph`, a new view of the acyclic graph that manages elimination. It allows actual elimination between sort variables, and even though this PR does not introduce...
This PR makes substantial changes to `lra` so that is can handle Mixed Integer Linear Programs (MILP) i.e. goals where variables range over either R or Z. This requires several...
#### Description of the problem I have noticed, while working with `Reals` that my `Search` queries are polluted by lemmas which (i think) were generated from an `Add Field` command....
### Is your feature request related to a problem? Having `Extraction TestCompile` work for Haskell (along with a way to add `+RTS -M9G -RTS` to ghc command-line flags) would allow...
