Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Borrow annotations for non-external declarations #538

Open
Kha opened this issue Jun 18, 2021 · 1 comment
Open

Borrow annotations for non-external declarations #538

Kha opened this issue Jun 18, 2021 · 1 comment
Labels
enhancement New feature or request

Comments

@Kha
Copy link
Member

Kha commented Jun 18, 2021

Would help with eliding unnecessary inc/decs for e.g. ReaderT arguments

lean_object *l_Lean_Elab_Term_Do_ToCodeBlock_concatWith(
    lean_object *x_1, lean_object *x_2, lean_object *x_3, lean_object *x_4,
    lean_object *x_5, lean_object *x_6, lean_object *x_7, lean_object *x_8,
    lean_object *x_9, lean_object *x_10) {
_start : {
  if (lean_obj_tag(x_2) == 0) {
    lean_object *x_11;
    lean_dec(x_9);
    lean_dec(x_8);
    lean_dec(x_7);
    lean_dec(x_6);
    lean_dec(x_5);
    lean_dec(x_4);
    lean_dec(x_3);
    x_11 = lean_alloc_ctor(0, 2, 0);
    lean_ctor_set(x_11, 0, x_1);
    lean_ctor_set(x_11, 1, x_10);
    return x_11;
...
@Kha Kha added the enhancement New feature or request label Jun 21, 2021
@leodemoura
Copy link
Member

This is a must-have feature. It is part of the (now delayed) compiler refactoring project.

ChrisHughes24 pushed a commit to ChrisHughes24/lean4 that referenced this issue Dec 2, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
Compiler refactoring
Awaiting triage
Development

No branches or pull requests

2 participants