• Heiko Becker's avatar
    Add two new inference function inferErrorbound and inferIntervalbound. · 724d0058
    Heiko Becker authored
    The functions can be used to generate HOL4 level certificates without stepping
    out of the logic and calling Daisy. As the functions are not verified their
    returned certificate should still be send through the checker pipeline.
    The sole benefit of the functions is that they can be used as in-logic
    generators for checker input.