blob: 60f26a0010e1ad42e023aaa54738ce65db0bf3be (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
// RUN: %dafny /compile:0 /autoTriggers:1 /noNLarith "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
function power(n:nat, e:nat) : int
lemma lemma_power()
ensures forall n:nat, e:nat :: 0 <= n * e && power(n, e) == 5;
{
forall n:nat, e:nat
ensures 0 <= n * e && power(n, e) == 5;
{
assume false;
}
}
|