Comments (2)
Even if external contributions are not welcome at the moment, there is no reason to hide the code.
from lean4.
but... why do you want to contribute in the first place ?
from lean4.
Related Issues (20)
- Kernel error from dependent pattern match
- Fields having inductive types with trivial structure are always stored boxed HOT 1
- `lake clean` should remove `lakefile.olean` in the root directory and under `lake-packages` HOT 3
- `lake update` permutes packages in `lake-manifest.json` HOT 2
- RFC: please add commutativity theorems about addition and multiplication of `Int`s to the Prelude HOT 3
- "compiler IR check failed" error when trying to create `ToString` instance HOT 1
- ident treated as token (e.g. `str` as a string) with `behavior := symbol` HOT 2
- `(kernel) declaration has free variables` error when extending class with typeclass parameter and extends HOT 2
- Strange error message from simp_arith HOT 2
- Slight change to typeclass use slows down 15 seconds -> 5 minutes HOT 4
- RFC: built in option to suppress compilation of defs HOT 1
- RFC: add the option to add a prefix and a suffix to a doc-string when using `inherit_doc` HOT 3
- Matching on a constructor that takes an instance argument using swift notation wrongfully tries to synthesize the instance
- `rfl` runtime increases exponentially, causing `timeout at 'whnf'` HOT 2
- (kernel) unknown constant in mutually recursive definition HOT 2
- compiler slowdown optimizing Option/List uses HOT 1
- Lake segmentation fault HOT 19
- `simp` fails when custom discharger makes no progress HOT 5
- RFC: Allow trailing comma after the last element of a list HOT 6
- validate project names HOT 2
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 lean4.