Test/triggers/splitting-picks-the-right-tokens.dfy


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

// This file ensures that trigger splitting picks the right tokens

function Id(i: int): int { i }

method MSuchThat()
  requires forall x | x > 0 :: Id(x) > 1 && x > 2 && x > -1 { }

method MImplies()
  // The bodies of the two terms that are produced here are both
  // BinaryExpressions(==>); the token they use, however, is that of the RHS
  // terms of these implications; otherwise, error messages would get stacked on
  // the ==> sign
  requires forall x :: x > 0 ==> Id(x) > 1 && x > 2 && x > -1 { }

method M() {
  if * {
    MImplies();
  } else {
    MSuchThat();
  }
}