File tree Expand file tree Collapse file tree 4 files changed +11
-11
lines changed Expand file tree Collapse file tree 4 files changed +11
-11
lines changed File renamed without changes.
Original file line number Diff line number Diff line change 1- Require Import preloaded .
1+ Require Import Preloaded .
22
33Lemma solution : 1 + 1 = 3.
44Proof . firstorder using test_axiom. Qed .
Original file line number Diff line number Diff line change 1- Require solution .
2- Require Import preloaded .
1+ Require Solution .
2+ Require Import Preloaded .
33From CW Require Import Loader.
44
5- CWGroup "Tests for solution .solution".
5+ CWGroup "Tests for Solution .solution".
66 CWTestCase "Type test".
7- Fail CWAssert "Should fail" solution .solution : (1 + 1 = 2).
8- CWAssert solution .solution : (1 + 1 = 3).
7+ Fail CWAssert "Should fail" Solution .solution : (1 + 1 = 2).
8+ CWAssert Solution .solution : (1 + 1 = 3).
99 CWTestCase "Assumptions test".
10- CWAssert "Testing solution" solution .solution Assumes test_axiom.
10+ CWAssert "Testing solution" Solution .solution Assumes test_axiom.
1111CWEndGroup.
1212
13- Definition solution_test := solution .solution.
13+ Definition solution_test := Solution .solution.
1414
1515CWGroup "Another test
1616with line breaks".
Original file line number Diff line number Diff line change 1- coqc preloaded .v
2- coqc solution .v
3- coqc -I ../src -Q ../theories CW test .v
1+ coqc Preloaded .v
2+ coqc Solution .v
3+ coqc -I ../src -Q ../theories CW SolutionTest .v
You can’t perform that action at this time.
0 commit comments