Mentions légales du service

Skip to content
  • Andrei Paskevich's avatar
    put built-in theories and modules under the library path "why3" · 3df85aba
    Andrei Paskevich authored
    In this way, we can always distinguish them from local theories and
    modules. Both 'use Bool' and 'use why3.Bool' are accepted. No support
    for use/clone of built-in modules is done yet, but so far we don't
    needed (the only built-in module is why3.Prelude which is used by
    default).
    
    As of now, one cannot put a file "why3.why" at the root of loadpath,
    since it will be inaccessible. Paths like why3/toto.why are still
    admitted, but we will probably ban them too and reserve the whole
    "why3.xxx.yyy" hierarchy for the built-in theories and modules.
    3df85aba