blob: b72203350f026288568baa9cce017ff220ab14a3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
// RUN: %dafny /noNLarith /z3opt:pi.warnings=true /proverWarnings:1 /compile:0 /autoTriggers:1 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
function GetIndexInSequence<T>(s:seq<T>, x:T) : int
requires x in s;
ensures 0 <= GetIndexInSequence(s, x) < |s|;
ensures s[GetIndexInSequence(s, x)] == x; {
var i :| 0 <= i < |s| && s[i] == x;
i
}
|
