• 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.
    9c20cd7c
Name
Last commit
Last update
bench Loading commit data...
bin Loading commit data...
comparison Loading commit data...
doc Loading commit data...
drivers Loading commit data...
examples Loading commit data...
lib Loading commit data...
misc Loading commit data...
modules Loading commit data...
plugins Loading commit data...
share Loading commit data...
src Loading commit data...
tests Loading commit data...
theories Loading commit data...
.gitignore Loading commit data...
AUTHORS Loading commit data...
CHANGES Loading commit data...
DEVELOPER.readme Loading commit data...
INSTALL Loading commit data...
LICENSE Loading commit data...
Makefile.in Loading commit data...
OCAML-LICENSE Loading commit data...
README Loading commit data...
ROADMAP Loading commit data...
TODO Loading commit data...
Version Loading commit data...
check.sh Loading commit data...
configure.in Loading commit data...