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...
While I was trying to execute make, this happens. ``` OCAMLOPT kernel/univ.ml File "kernel/univ.ml", line 302, characters 16-21: Error: Multiple definition of the extension constructor name Found. Names must be...
``` coq Require Import HoTT. Goal True. Proof. assert {m:nat & True} as n. exists 0. exact tt. transparent assert (H: True). destruct n. (* Anomaly: variable n unbound. Please...
``` coq (* File reduced by coq-bug-finder from original input, then from 8249 lines to 907 lines, then from 843 lines to 357 lines, then from\ 351 lines to 260...
The following code works in coq 8.4, but not in HoTT/coq: ``` coq Set Implicit Arguments. Set Universe Polymorphism. Generalizable All Variables. Record SpecializedCategory (obj : Type) := { Object...
This code fails in HoTT/Coq, but does not if I remove the `change` (`present_obj`) or `intros` lines: ``` Coq Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. Polymorphic Record...
``` coq (* File reduced by coq-bug-finder from 520 lines to 9 lines. *) Set Universe Polymorphism. Class IsPointed (A : Type) := point : A. Generalizable Variables A B...
I have an example at https://gist.github.com/JasonGross/8852236 (very bottom) where the unification engine churns for 3-4 seconds before deciding that terms are unifiable. I'm not sure if anything can be done...
At https://github.com/JasonGross/HoTT/tree/be130e7b72e8b5bf804e3612b095de0ba01d864c, `time ./hoqtop < theories/categories/Limits/Functors.v` finishes in under 1 second, while `hoqc theories/categories/Limits/Functors.v` spins for a quite a while.
If we provide a syntax for explicit universe levels, @mattam82 has said that he will provide it. I propose something like the following: ``` coq Definition foo {universes i
Here is some code that works on HoTT/coq trunk, fails on `pose (@isequiv_apD10 H (Lift A)).` with polyproj, and fails on `exact t'` with polyproj when we replace the standard...