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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 31 Jul 2019 08:42:57 +0200*References*: <61020587-764f-43bf-859f-24001b37baa4@googlegroups.com> <50ACB5BD-FAE7-4BD1-B471-BE58CE03D7AE@gmail.com> <d3afd887-ba2f-4b58-b001-b5484a6f5da1@googlegroups.com>

For introducing new identifiers in assumptions you can write NEW [ CONSTANT | STATE | VARIABLE | ACTION | TEMPORAL ] <id> and if you don't specify a level, it defaults to CONSTANT. For a state-level formula such as an invariant, you want to write NEW STATE Inv Regards, Stephan
-- 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/32628BBC-D4E2-4D10-8361-A15125D09CB7%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Meta-theorem (induction lemma) in TLA+***From:*shinsa82

**References**:**[tlaplus] Meta-theorem (induction lemma) in TLA+***From:*shinsa82

**Re: [tlaplus] Meta-theorem (induction lemma) in TLA+***From:*Stephan Merz

**Re: [tlaplus] Meta-theorem (induction lemma) in TLA+***From:*shinsa82

- Prev by Date:
**Re: [tlaplus] Meta-theorem (induction lemma) in TLA+** - Next by Date:
**Re: [tlaplus] Trying to follow along with INRIA's TLAPS tutorial** - Previous by thread:
**Re: [tlaplus] Meta-theorem (induction lemma) in TLA+** - Next by thread:
**Re: [tlaplus] Meta-theorem (induction lemma) in TLA+** - Index(es):