1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
// RUN: %dafny /compile:0 /autoTriggers:1 /print:"%t.print" "%s" > "%t" // RUN: %diff "%s.expect" "%t" predicate IsLessThanSuccesor(i:int) { i < i + 1 } lemma LemmaWithoutTriggerOnForallStatement() { forall i ensures IsLessThanSuccesor(i); { } }