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

from method provided by core::convert::From is not extracted to the same name if it passed as a closure #1165

Open
maximebuyse opened this issue Dec 3, 2024 · 2 comments
Labels
bug Something isn't working engine Issue in the engine f* F* backend

Comments

@maximebuyse
Copy link
Contributor

struct A();

impl From<()> for A {
    fn from(x: ()) -> A {
        A()
    }
}

fn test(x: Option<()>) -> Option<A> {
    match x {
        Some(v) => Some(A::from(v)),
        None => None
    }
}
fn test2(x: Option<()>) -> Option<A> {
    x.map(A::from)
}

Open this code snippet in the playground

In the example above, from of test is extracted as Core.Convert.f_from in f* (which is provided by our Core lib. But in test2 it yields Core.Convert.From.from which we don't have

@maximebuyse maximebuyse added bug Something isn't working engine Issue in the engine f* F* backend labels Dec 3, 2024
@W95Psp
Copy link
Collaborator

W95Psp commented Dec 3, 2024

I think this is #991

@franziskuskiefer
Copy link
Member

Use the following workaround for now

fn test2(x: Option<()>) -> Option<A> {
    x.map(|v| A::from(v))
}

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working engine Issue in the engine f* F* backend
Projects
None yet
Development

No branches or pull requests

3 participants