[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] << >> = { }

 The theory of functions in TLAPS (more precisely, in the Isabelle backend of TLAPS, which we consider as the standard), is axiomatized in precisely this way, plus the related definitions of [S -> T] and the EXCEPT construct. I'd therefore object to your assertion that the theory is defined semantically rather than axiomatically.

I'll try to write a list of all the axioms and definitions used by TLA+. Simply for clarity's sake. A list such as:

axiom ax-1 ...

axiom ax-2 ...

definition df-1 ...

And so on. If I succeed. I'll post it here.