Test de real.Abs en PVS

520936e9 · MARCHE Claude · e0279f0b · 520936e9
Commit 520936e9 authored Dec 11, 2013 by MARCHE Claude
Hide whitespace changes
Inline Side-by-side

Showing with 10 additions and 0 deletions

tests/test-claude.why tests/test-claude.why +10 -0

No files found.
--- a/tests/test-claude.why
+++ b/tests/test-claude.why
@@ -228,3 +228,13 @@ theory TestWarnings
  lemma L2 : exists x:t. x=x -> false

 end
+
+theory TestPVSRealAbs
+
+  use import int.Abs
+  use import real.RealInfix
+  use import real.Abs as A
+
+  lemma l: A.abs (-. 1.0) = 1.0
+
+end
\ No newline at end of file