Claude Marche
fc857b2fc2
proved udivexact generique
2025-11-25 11:26:25 +01:00
Claude Marche
b9feb6aece
proved mul generique
2025-11-25 10:49:15 +01:00
Claude Marche
d17a7b64b7
redone sum_accuracy and g_accuracy
2025-11-24 11:33:09 +01:00
Claude Marche
9c60b5f0d6
add propagation in any format
2025-11-24 10:51:55 +01:00
Claude Marche
e1d543c06f
SLSE full proof
...
generalize hypothesis on size, depending on value of eps
2025-03-10 16:00:09 +01:00
Matteo Manighetti
7ae65be566
Upgrade sessions to use Alt-Ergo 2.6.0
2025-01-14 19:48:35 +01:00
MARCHE Claude
9161acda8e
Add metas for unused dependencies in generated axioms
2024-10-25 18:34:29 +02:00
MARCHE Claude
6813754dce
clarify ghost and non-ghost for reals and ufloats
2024-10-01 15:38:42 +02:00
Claude Marche
45f773f588
improve readibility, and various small improvements
2024-06-21 14:38:55 +02:00
BONNOT Paul
f24be4fce6
SLSE example : simplify proof
2024-06-18 13:41:01 +02:00
Paul Bonnot
7c3e02999d
Remove higher order
2024-06-10 16:44:04 +02:00
Claude Marche
4d68a5a802
disabled Alt-Ergo FPA for versions < 2.5.4 (bug known)
2024-05-23 11:17:31 +02:00
MARCHE Claude
85916f62c6
never encode enums and records for Alt-Ergo
2024-05-22 12:18:37 +02:00
Paul Bonnot
103af257d0
Removed inline_trivial
2024-04-22 17:41:45 +02:00
Claude Marche
2a1637b43d
remove useless hint
2024-04-16 12:58:50 +02:00
BONNOT Paul
79666d1218
Resolve "forward_propagation strategy : sin and cos support"
2024-03-28 15:49:24 +01:00
BONNOT Paul
2e4dad7111
Improve the support for unbounded floats and forward error propagation strategy
...
Unbounded floats theories for single resp double precision are now clones of a
generic module parameterized by epsilon and eta
Add support for exp and log in the strategy
Add more examples of use in examples/numeric
Documentation of the strategy in the manual
Documentation of ufloat in the stdlib
Documentation of session/strategy.mli in the API doc
2024-03-06 12:09:41 +01:00
BONNOT Paul
e4429e7dda
Resolve "Forward error propagation strategy : Sum, Exp, Log"
...
new lemmas on real exp and log
examples of use
2024-02-23 13:01:05 +01:00
BONNOT Paul
85c4b4917a
Forward propagation of rounding errors
...
New theory for unbounded floats, with propagation lemmas
Examples of use
2024-01-18 10:31:14 +00:00
