Skip to content
Snippets Groups Projects
  • Etienne Kneuss's avatar
    449725fe
    Do not ignore all implicits, only implicit synthetic functions. · 449725fe
    Etienne Kneuss authored
    > @ignore
    > implicit class Foo(x: ..)
    
    generates an implicit synthetic conversion without @ignore. We
    explicitly ignore these as they are extracted specially. However, we
    should *not* ignore implicit defs that the user defined for convenience.
    
    Sadly, Scala does not support "implicit case class", so in Leon
    you have to use a normal case class with a normal implicit conversion
    that wraps in the case-class:
    
    > case class Foo(x: Bar)
    > implicit def barToFoo(b: Bar): Foo = Foo(b)
    449725fe
    History
    Do not ignore all implicits, only implicit synthetic functions.
    Etienne Kneuss authored
    > @ignore
    > implicit class Foo(x: ..)
    
    generates an implicit synthetic conversion without @ignore. We
    explicitly ignore these as they are extracted specially. However, we
    should *not* ignore implicit defs that the user defined for convenience.
    
    Sadly, Scala does not support "implicit case class", so in Leon
    you have to use a normal case class with a normal implicit conversion
    that wraps in the case-class:
    
    > case class Foo(x: Bar)
    > implicit def barToFoo(b: Bar): Foo = Foo(b)