From here: #61 (comment)
ewd998, which runs into a naming collision between the TLAPS and community modules. Specifically Functions.tla; it tries to use operators in the Community version of Functions.tla, while also importing various modules from the TLAPS standard library (which itself includes a Functions.tla that doesn't have those operators).
I confirm that the name clash between the TLAPS standard theorem library and some of the Community Modules (in particular Functions) is known and should be fixed in the long overdue release of TLAPS.
From here: #61 (comment)