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...
The main objective of the PR is to replace the notation arguments of possible atomic type constr, pattern, and binders by an algebra of types based on the same atoms...
Another solution for #18855 which does not rely on making `term_of_fconstr` complete. Requires #19410 (this PR is what made me discover the issue).
Not 100% sure that this is correct, but this fixes an issue (using code from another branch so I can't put it in the test-suite)
As shown in #16935, the interpretation of references in Ltac functions happens to be different in strict mode (i.e., in practice, non interactively) and in non-strict mode (i.e., in practice,...
As the test points out, the projected can be typed, but its type not reduce to an applied inductive. In vanilla Coq this can happen because of unif constraints.
~~~coq Inductive even (x : bool) : nat -> Type := | evenO : even x 0 | evenS : forall n, odd x n -> even x (S n)...
### Description of the problem _No response_ ### Small Coq file to reproduce the bug ```coq #[projections(primitive=yes)] Class Lens (a b c d : Type) : Type := { view...
I have finished the practices of `sf/lf` and part of `sf/plf`, and I'm familiar with many other language's module system, such as haskell/python/javascript, but still can't grasp Coq's module system,...
