Jason Gross
Jason Gross
``` coq Monomorphic Definition U1 := Type. Monomorphic Definition U2 := Type. Set Printing Universes. Monomorphic Definition foo : True. pose ((U1 : U2)). Print Universes. (* Prop < Set...
``` coq Set Printing Universes. Monomorphic Definition U1 := Type. Monomorphic Definition U2 := Type. Definition bar := U1 : U2. Definition baz := U2 : U1. (* This works!!!!...
I would like tactics which unify universes. I can do it now with the following notations: ``` coq Polymorphic Definition type_of {A} (_ : A) := A. Notation unify_universes t1...
Am I supposed to see `Algebraic universe on the right`? The following code fails at `Defined` (it should probably fail to `pose`?), but prints out `Algebraic universe on the right`...
I have some code in a file `Functor.v`, that when I change two lemmas from `Lemma foo : fooT. ... Qed.` to `Lemma foo : fooT. ... Defined. Global Opaque...
Is there any plan to have explicit universe level variables in Coq? Alternatively, is there a way to get the following approach to "work"? ``` Coq Set Implicit Arguments. Set...
This works in Coq 8.4, but not HoTT/coq. The fragment of the code in #36 which reproduces this is: ``` coq Set Implicit Arguments. Set Universe Polymorphism. Generalizable All Variables....
If bug05.v is ``` coq Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. Set Universe Polymorphism. Delimit Scope object_scope with object. Delimit Scope morphism_scope with morphism. Delimit Scope category_scope...
It takes about 24 seconds on my machine, which is about 10% of the total time spent building util files in fiat-crypto (and is 1.5x slower than the next-slowest file)....
This unfortunately makes src/riscv/Spec/Decode.v a bit slower; I can speed it up if desired by setting boolean equality only for `InstructionSet`. This is to help with https://github.com/mit-plv/bedrock2/issues/285 ... which I...