Mentions légales du service

Skip to content
  • Andrei Paskevich's avatar
    Task: use "Use" to represent theory use · d993dad4
    Andrei Paskevich authored
    up to this point, we used Clone declarations with an empty substitution
    to represent use of theories in tasks. The intention was to stress the
    fact that the imported declarations are physically present in the task
    and thus are followed by a "witness" Clone declaration (whereas a Use
    inside a theory acts rather as a pointer to follow).
    
    However, this encoding requires the clone substitution to cover every
    locally defined symbol: otherwise we might not be able to distinguish
    a use from a clone. Therefore, we had to clone even Pgoal propositions
    as Pskip, in order to keep the substitutions complete.
    
    This commit restricts the Clone declarations in tasks to actual
    theory cloning, and represents theory use with Use declarations.
    This hopefully makes the API more clear, and will allow us to
    abolish Pskip.
    d993dad4