Comments (3)
Nadrieril
commented on September 13, 2024
We can likely replace all Copy bounds with Clone bounds, but is that an improvement? Your type signature would stay roughly the same
from aeneas.
Nadrieril
commented on September 13, 2024
Maybe a --discard-unused-bounds flag on Charon would make sense, under which we could often remove the Copy bounds altogether
from aeneas.
RaitoBezarius
commented on September 13, 2024
@Nadrieril Discussed with @sonmarcho today too, yeah, I guess at most, discarding the unused bounds is the best thing that can be done.
Alternatively, applying a linter on the resulting extraction code will achieve something similar.
from aeneas.
Related Issues (20)
- Use `omega` instead of `linarith` in the `scalar_tac` tactic HOT 1
- Add String to the Lean library
- Support non-primitive `Copy` types
- Update the CI to format the code and check that there are no compilation warnings
- Update the CI to check there is no diff in the generated files HOT 2
- Use the option `-check-inv` on the tests only in CI
- Uncompilable Lean involving `Option::take`
- Trait overriding from the libstd is not supported HOT 1
- Failure when extracting a loop with a shared borrow HOT 1
- `core::mem::swap` is not supported
- `Option::is_none` is unsupported
- Usage of `as` in Lean can cause syntactical errors HOT 3
- `Scalar.cut` does not exist HOT 2
- Add a Contributing.md file
- Easy installation recipes HOT 5
- Failure when extracting a loop HOT 1
- Check in CI that the build doesn't generate warnings HOT 1
- Don't run the same CI jobs twice
- Add a backend test for infinite loops
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 aeneas.