Comments (2)
I just realized that my comment at #1929 (comment) was confused. In that spot of that PR, what is being used is that op is involutive. Here, core5 is checking that core and op commute. So it's not weird that one of them (here) is slow while the other (in that PR) is fast. This one is probably slow simply because there is a huge amount to unpack. So this can probably be closed. (Although it would be nice if there was a way to make this fast...)
from coq-hott.
Yes, looking back I think you are right. The issue here which perplexes me is that all of these examples in the test are instant except for is1cat. I tried for an hour today to get a favourable manual reduction but the term is just so huge. I also tried tweaking the proofs Equiv.v about core so that they are as eta reduced as possible. I cannot workout why this is such a straining example for Coq.
from coq-hott.
Related Issues (20)
- Remove redundant fields from Ring
- Generalize lhs, lhs_V, rhs and rhs_V to all transitive relations HOT 2
- Define matrices as functions HOT 2
- Define matrices as a collection of columns rather than a collection of rows
- General Linear group HOT 1
- Finite fields (Galois fields)
- Prime numbers
- Idempotent ring elements
- grp_pow and related things HOT 9
- Tensor product of cyclic groups HOT 26
- use CongruenceQuotient to define coequalizer HOT 9
- Error: Unknown scope delimiting key _type. HOT 6
- Coq Platform and opam version lags HOT 5
- Add HasEquivs instance for MatrixCat HOT 1
- Binomial Coefficients
- Replace old definition of `cyclic` with new `cyclic'`
- Fundamental theorem of arithmetic HOT 1
- Add functorality of cokernels and quotients for AbGroup
- Allow subgroups to be defined by predicates that don't take values in h-props
- Prove that `n / (m / k) = (n * k) / m`
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from coq-hott.