• Andrei Paskevich's avatar
    "eliminate_epsilon" added in drivers · 9c20cd7c
    Andrei Paskevich authored
    Currently, the builtin theory why3.HighOrd (or just HighOrd) must
    be explicitly "use"-d. However, the type (HighOrd.func 'a 'b) can
    be written ('a -> 'b), and the type (HighOrd.pred 'a) can be written
    ('a -> bool), and the application operation (HighOrd.(@)) can be
    written as the usual juxtaposition. Thus, normally, you do not have
    to write the qualifiers. The builtin theory why3.Bool (or just Bool)
    is needed for "bool". The names "HighOrd", "func", "pred", and "(@)"
    are not yet fixed and may change.
    "eliminate_epsilon" tries to be smart when a lambda (or some other
    comprehension form) occurs under equality or at the top of a definition.
    We could go even further and replace (\ x . t) s with t[x <- s], without
    lifting the lambda. I'm not sure it's worth it: we rarely write redexes
    manually. They can and will appear through inlining, though.
    Anyone who wants to construct epsilon-terms directly using the API
    should remember that these are not Hilbert's epsilons: by writing
    an epsilon term, you postulate the existence (though not necessarily
    uniqueness) of the described object, and "eliminate_epsilon" will
    happily convert it to an axiom expressing this existence. We only
    use epsilons to write comprehensions whose soundness is guaranteed
    by a background theory, e.g. lambda-calculus.
pvs-common.gen 7.62 KB