Skip to content
Snippets Groups Projects
  • Etienne Kneuss's avatar
    027c0d4c
    Implement the Leon library. Support classes and methods. · 027c0d4c
    Etienne Kneuss authored
    - Implement the Leon Library in Leon-land rather than Scala-land.
      import leon.Utils._ becomes import leon.lang._
      import leon.Annotations._ becomes import leon.annontation._
    
      For now, the library defines generic Options and Lists.
      The library is automatically imported from the ./leon script, unless
      the --library=no option is passed.
    
    - Support parsing of multiple files and modules.
    
    - Introduce new annontations:
        @ignore: remove definition from Leon
        @verified: do not consider for verification unless explicitly
            specified
    027c0d4c
    History
    Implement the Leon library. Support classes and methods.
    Etienne Kneuss authored
    - Implement the Leon Library in Leon-land rather than Scala-land.
      import leon.Utils._ becomes import leon.lang._
      import leon.Annotations._ becomes import leon.annontation._
    
      For now, the library defines generic Options and Lists.
      The library is automatically imported from the ./leon script, unless
      the --library=no option is passed.
    
    - Support parsing of multiple files and modules.
    
    - Introduce new annontations:
        @ignore: remove definition from Leon
        @verified: do not consider for verification unless explicitly
            specified