From ce1902574f926062daa4a1373e5ffface102d1e7 Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Sat, 13 Apr 2013 14:46:05 +1000 Subject: [PATCH] A test-case demonstrating the problem with github issue #115. Currently failing so I've put this onto a branch of its own. --- src/boss/theory_tests/github115aScript.sml | 14 ++++++++++++++ src/boss/theory_tests/github115bScript.sml | 15 +++++++++++++++ 2 files changed, 29 insertions(+) create mode 100644 src/boss/theory_tests/github115aScript.sml create mode 100644 src/boss/theory_tests/github115bScript.sml diff --git a/src/boss/theory_tests/github115aScript.sml b/src/boss/theory_tests/github115aScript.sml new file mode 100644 index 0000000000..1c9cc8b20b --- /dev/null +++ b/src/boss/theory_tests/github115aScript.sml @@ -0,0 +1,14 @@ +open HolKernel Parse boolLib bossLib + +val _ = new_theory "github115a" + +open arithmeticTheory + +val _ = overload_on ("foo", ``\x. x + y``) + +val sample = store_thm( + "sample", + ``!y:bool. foo x < foo z ==> x < z``, + SRW_TAC [ARITH_ss][]) + +val _ = export_theory() diff --git a/src/boss/theory_tests/github115bScript.sml b/src/boss/theory_tests/github115bScript.sml new file mode 100644 index 0000000000..c3f1bf8882 --- /dev/null +++ b/src/boss/theory_tests/github115bScript.sml @@ -0,0 +1,15 @@ +open HolKernel Parse boolLib bossLib + +open github115aTheory + +(* this theory is in the test-case solely to force Holmake to check that the + github115aTheory.sml file is loadable (it isn't when the bug is evident + because the exception in the execution of export_theory results in a + corrupt Theory.sml file) +*) + +val _ = new_theory "github115b" + +val sample2 = save_thm("sample2", AND_CLAUSES) + +val _ = export_theory()