File tree Expand file tree Collapse file tree 3 files changed +24
-20
lines changed Expand file tree Collapse file tree 3 files changed +24
-20
lines changed Original file line number Diff line number Diff line change 2626
2727empty = {}.
2828
29- expect = galaxy expect = {}. end
30- tested :: empty [expect].
29+ tested :=: {}.
3130tested = process #e. #a1. #kill. end
3231
33- expect = galaxy expect = {}. end
34- tested :: empty [expect].
32+ tested :=: {}.
3533tested = process #0. #a1. #kill. end
3634
37- expect = galaxy expect = {}. end
38- tested :: empty [expect].
35+ tested :=: {}.
3936tested = process #1. #a1. #kill. end
4037
41- expect = galaxy expect = { accept }. end
42- tested :: empty [expect].
38+ tested :=: accept.
4339tested = process +i(0:0:0:e). #a1. #kill. end
4440
45- expect = galaxy expect = {}. end
46- tested :: empty [expect].
41+ tested :=: {}.
4742tested = process +i(0:1:0:e). #a1. #kill. end
4843
49- expect = galaxy expect = {}. end
50- tested :: empty [expect].
44+ tested :=: {}.
5145tested = process +i(1:1:0:e). #a1. #kill. end
Original file line number Diff line number Diff line change 1+ 1 = +nat(s(0)).
2+ 2 = +nat(s(s(0))).
3+ 3 = +nat(s(s(s(0)))).
4+
5+ nat = -nat(s(X)) +nat(X).
6+
7+ tested :=: +nat(0).
8+ tested = linear-exec #1 #nat end
9+
10+ tested :=: +nat(s(0)).
11+ tested = linear-exec #2 #nat end
12+
13+ tested :=: +nat(s(s(0))).
14+ tested = linear-exec #3 #nat end
Original file line number Diff line number Diff line change 55
66empty = {}.
77
8- expect = galaxy expect = 0. end
9- tested :: empty [expect].
8+ tested :=: 0.
109tested = #add (@-add(0 0 R) R).
1110
12- expect = galaxy expect = s(0). end
13- tested :: empty [expect].
11+ tested :=: s(0).
1412tested = #add (@-add(s(0) 0 R) R).
1513
16- expect = galaxy expect = s(0). end
17- tested :: empty [expect].
14+ tested :=: s(0).
1815tested = #add (@-add(0 s(0) R) R).
1916
20- expect = galaxy expect = s(s(s(s(0)))). end
21- tested :: empty [expect].
17+ tested :=: s(s(s(s(0)))).
2218tested = #add (@-add(s(s(0)) s(s(0)) R) R).
You can’t perform that action at this time.
0 commit comments