Tried to check this proof as well. But I'm getting the following error
when using tlapm from the updated_enabled_cdot branch.
As I understand, this branch is going to be the basis for the next
release, thus I hope this report will be useful.
(* created new ".tlacache/TLAPS.tlaps/TLAPS.thy" *)
(* fingerprints written in ".tlacache/TLAPS.tlaps/fingerprints" *)
File "/home/karolis/CODE/pub/tlapm/tmp/lib/tlaps/TLAPS.tla", line 1,
character 1 to line 362, character 77:
[INFO]: All 0 obligation proved.
tlapm ending abnormally with Invalid_argument("List.combine")
Raised at file "
stdlib.ml", line 30, characters 20-45
Called from file "
list.ml", line 263, characters 36-49
Called from file "
e_levels.ml", line 228, characters 28-55
Called from file "
e_levels.ml", line 234, characters 27-55
Called from file "
e_levels.ml", line 413, characters 21-30
Called from file "
e_levels.ml", line 934, characters 21-30
Called from file "
e_levels.ml", line 992, characters 26-35
Called from file "
e_visit.ml", line 222, characters 23-31
Called from file "
e_visit.ml", line 223, characters 24-33
...
Called from file "
e_visit.ml", line 223, characters 24-33
Called from file "
e_visit.ml", line 146, characters 22-31
Called from file "
e_levels.ml", line 560, characters 27-39
Called from file "
prep.ml", line 1373, characters 12-42
Called from file "
prep.ml", line 1458, characters 51-70
Called from file "camlinternalLazy.ml", line 29, characters 17-27
Re-raised at file "camlinternalLazy.ml", line 36, characters 4-11
Called from file "
schedule.ml", line 83, characters 17-24
Called from file "
schedule.ml", line 141, characters 37-62
Called from file "
schedule.ml", line 181, characters 4-14
Called from file "
tlapm.ml", line 208, characters 4-42
Called from file "
tlapm.ml", line 408, characters 12-77
Called from file "
tlapm.ml", line 503, characters 23-43
Called from file "
list.ml", line 121, characters 24-34
Called from file "
tlapm.ml", line 506, characters 13-40
Called from file "
tlapm.ml", line 518, characters 8-33
> To view this discussion on the web visit
https://groups.google.com/d/msgid/tlaplus/84f326ac-a2f8-4966-a8c5-fa33a3d6c3c4n%40googlegroups.com.