Comments (1)
Kha
commented on August 19, 2024
I'm closing this since this will simply lead to another dependency cycle: PPExt -> CoreM -> Message -> PPExt. We would have to split at least Message and Util.Trace to circumvent it. It's probably easier to only use direct invocations when testing and tracing the pretty printer.
from lean4.
Related Issues (20)
- Lemmas about `private` defs are not `private` by default HOT 2
- Bug: 'unterminated comment' error when you have `/-` in a docstring HOT 2
- RFC: Use emoji variant selector for unicode characters HOT 4
- RFC: global diagnostics HOT 4
- Hovering over the `_` in `?_` shows irrelevant docstring
- `rw [def]` only works with first applicable equation lemma HOT 1
- default termination tactic: array_dec_dec tactic too eager, and too weak HOT 1
- bug: metavariable context being rolled back in simp
- typeclass inference crashes HOT 2
- Regression in inferring universe levels between v4.9.1 and v4.10.0-rc1 HOT 1
- decreasing_by goal with nested recursion mentions internal induction hypothesis
- RFC: remove `simpCtorEq` from the default simprocs HOT 1
- Broken Lake linking
- Incorrect arg count in a functional induction match arm, when WF def uses local variables. HOT 2
- Inferred type of a variable not propagated to earlier usages HOT 1
- Exponential behavior in compilation HOT 1
- "Failed to generate splitter"
- Changing `internal.minimalSnapshots` option leads to a panic
- Incrementality causes a weird error
- Lake doesn't ensure that module roots are disjoint HOT 3
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.