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 is a sister draft PR of #16004, whose only goal is to check that the changes in CI devs are compatible with the switch of semantics. Eventually this should...
# Release checklist # ## When the release managers for version `X.X` get nominated ## - [x] Create a new issue to track the release process where you can copy-paste...
#### Description of the problem ```coq Goal forall (f : False -> False), exists x : True -> False, forall (v : False), x I = f v. intro F....
#### Description of the problem `instantiate` is currently crippled with regards to automation. I can write ```coq Goal exists n : nat, n = n. eexists ?[n]. instantiate (n:=1). ```...
#### Description of the problem Like #16357 ```coq Fixpoint fact (n : nat) := match n with 0 => 1 | S n' => n * fact n' end. Goal...
apparently the rules for the prelude are not generated: ``` File "dev/shim/dune", line 14, characters 0-384: 14 | (rule 15 | (targets coqc-prelude) 16 | (deps 17 | %{bin:coqc} 18...
#### Description of the problem ```coq Goal forall x : nat, let y := x in exists z : nat, let w := z in w = w -> True....
overlay: - https://github.com/coq-community/coq-dpdgraph/pull/107
