[tlaplus] why I cannot compare Nat with 0

[victor zhang <zhavictor@xxxxxxxxx>]

I have the following TLA+ code

```

Threads == {"t1", "t2"}

VARIABLE thread_states

ThreadStateVal == 
    [
        read_index: {Nat},
        write_index: {Nat}
    ]
    
Init ==

    thread_states [ t \in Threads |-> [ read_index |-> 0, write_index |-> 0] ]

TypeOK ==

    thread_states \in [Threads -> ThreadStateVal]

....

```

When I run the model, I got "Attempted to compare integer 0 with non-integer: Nat", not sure how to fix it, any help will be greatly appreciated.

Thanks!

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9a3c35b7-9168-4950-a65b-582b5919b293n%40googlegroups.com.