search

tlaplus / CommunityModules

TLA+ snippets, operators, and modules contributed and curated by the TLA+ community
MIT License
273 stars 36 forks source link

Add `SequencesExt!FirstMatch` #40

Closed lemmy closed 3 years ago

lemmy commented 3 years ago 
---- MODULE SequencesExt ----

...

FirstMatch(s, P(_)) ==
  IF { i \in 1..Len(s) : P(s[i]) } # {}
  THEN Min( { i \in 1..Len(s) : P(s[i]) } )
  ELSE 0

====
lemmy commented 3 years ago

Obsolete