coq
coq copied to clipboard
HoTT
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 following proof script checks fine when indices-matter is disabled, but gives an error when it is turned on. ``` coq Inductive Empty : Type :=. Inductive paths {A :...
I want the following code to work: ``` coq Goal Type = Type. match goal with |- ?x = ?x => idtac end. ``` I'm not sure what the behavior...
Example file in [this repo](https://gist.github.com/jcmckeown/5843795).
Here is some code that works in 8.4 and not in trunk-polyproj: ``` coq (* File reduced by coq-bug-finder from 64 lines to 30 lines. *) Set Implicit Arguments. Set...
This code works in HoTT/coq trunk, but not trunk-polyproj (is this the inductive problem of https://github.com/HoTT/coq/issues/95#issuecomment-39706988?) ``` coq Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Record SpecializedCategory (obj...
``` coq (* File reduced by coq-bug-finder from 335 lines to 115 lines. *) Set Implicit Arguments. Set Universe Polymorphism. Generalizable All Variables. Record Category (obj : Type) := Build_Category...
``` coq (* File reduced by coq-bug-finder from 138 lines to 78 lines. *) Set Implicit Arguments. Generalizable All Variables. Set Universe Polymorphism. Delimit Scope object_scope with object. Delimit Scope...
The following code suffices to trigger it, on my system: ``` Definition my_fun (n:nat) := n. Section My_Sec. Global Arguments my_fun x : rename. End My_Sec. ``` The `Global Arguments`...
Sometimes I get `Cannot enforce tmpJT_kQC.10643 = Set because Set
``` coq Set Implicit Arguments. Set Universe Polymorphism. Notation idmap := (fun x => x). Inductive paths {A : Type} (a : A) : A -> Type := idpath :...